aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev
diff options
context:
space:
mode:
authorGravatar coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-03-07 14:39:58 +0000
committerGravatar coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7>2003-03-07 14:39:58 +0000
commit519af89c1395b85bc1b17041504096feaea01777 (patch)
treebf1f6091d527570296c8f9832354074e90056b20 /dev
parent525c6843d20132adb62d851e32b03c099395426f (diff)
Petites modifs de mes super-Makefiles ;)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3749 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev')
-rw-r--r--dev/Makefile.devel3
1 files changed, 2 insertions, 1 deletions
diff --git a/dev/Makefile.devel b/dev/Makefile.devel
index db25167f5..f3abb62dd 100644
--- a/dev/Makefile.devel
+++ b/dev/Makefile.devel
@@ -1,5 +1,6 @@
# to be linked to makefile (lowercase - takes precedence over Makefile)
# in main directory
+# make devel in main directory should do this for you.
TOPDIR=.
BASEDIR=
@@ -66,7 +67,7 @@ run: $(TOPDIR)/coqtop
usage::
- @echo " vars -- echos commands to set COQTOP and COQBIN variables"
+ @echo " vars -- echos commands to set COQTOP and COQBIN variables"
vars:
@(cd $(TOPDIR); \
echo export COQTOP=`pwd`/ ; \