aboutsummaryrefslogtreecommitdiff
path: root/docs/README.md
diff options
context:
space:
mode:
authorCyril Cohen2019-10-16 11:26:43 +0200
committerCyril Cohen2019-10-16 11:26:43 +0200
commit6b59540a2460633df4e3d8347cb4dfe2fb3a3afb (patch)
tree1239c1d5553d51a7d73f2f8b465f6a23178ff8a0 /docs/README.md
parentdd82aaeae7e9478efc178ce8430986649555b032 (diff)
removing everything but index which redirects to the new page
Diffstat (limited to 'docs/README.md')
-rw-r--r--docs/README.md6
1 files changed, 0 insertions, 6 deletions
diff --git a/docs/README.md b/docs/README.md
deleted file mode 100644
index 55e55b0..0000000
--- a/docs/README.md
+++ /dev/null
@@ -1,6 +0,0 @@
-This directory contains the website:
- http://math-comp.github.io/math-comp/
-What is committed in here goes straight online.
-
-By running make in htmldoc one updates the html files
-generated by coqdoc and the library graph.