aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/tools/Makefile.dir
diff options
context:
space:
mode:
Diffstat (limited to 'dev/tools/Makefile.dir')
-rw-r--r--dev/tools/Makefile.dir4
1 files changed, 2 insertions, 2 deletions
diff --git a/dev/tools/Makefile.dir b/dev/tools/Makefile.dir
index 68c917ac8..1a1bb90b4 100644
--- a/dev/tools/Makefile.dir
+++ b/dev/tools/Makefile.dir
@@ -1,6 +1,6 @@
# make a link to this file if you are working hard in one directory of Coq
-# ln -s ../dev/Makefile.dir Makefile
-# if you are working in a sub/dir/ make a link to dev/Makefile.subdir instead
+# ln -s ../dev/tools/Makefile.dir Makefile
+# if you are working in a sub/dir/ make a link to dev/tools/Makefile.subdir instead
# this Makefile provides many useful facilities to develop Coq
# it is not completely compatible with .ml4 files unfortunately