diff options
author | coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-03-07 14:39:58 +0000 |
---|---|---|
committer | coq <coq@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-03-07 14:39:58 +0000 |
commit | 519af89c1395b85bc1b17041504096feaea01777 (patch) | |
tree | bf1f6091d527570296c8f9832354074e90056b20 /dev | |
parent | 525c6843d20132adb62d851e32b03c099395426f (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.devel | 3 |
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`/ ; \ |