diff options
| author | herbelin | 2006-09-29 13:52:40 +0000 |
|---|---|---|
| committer | herbelin | 2006-09-29 13:52:40 +0000 |
| commit | 6281399f8a71a66d93461f6501372174f1508362 (patch) | |
| tree | 529c5d044ba9f443089e14ecb9bdd43518be4292 /dev/tools/Makefile.devel | |
| parent | 8746bc44bbfa32a0d8b06eeb61f0a12765c2f747 (diff) | |
Reactivation des outils de developpement de Jacek
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9190 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'dev/tools/Makefile.devel')
| -rw-r--r-- | dev/tools/Makefile.devel | 16 |
1 files changed, 8 insertions, 8 deletions
diff --git a/dev/tools/Makefile.devel b/dev/tools/Makefile.devel index f3abb62dd8..8dcc70cf7f 100644 --- a/dev/tools/Makefile.devel +++ b/dev/tools/Makefile.devel @@ -16,9 +16,9 @@ usage:: usage:: @echo " setup-devel -- set the devel makefile" setup-devel: - @ln -sfv dev/Makefile.devel makefile + @ln -sfv dev/tools/Makefile.devel makefile @(for i in $(SOURCEDIRS); do \ - (cd $(TOPDIR)/$$i; ln -sfv ../dev/Makefile.dir Makefile) \ + (cd $(TOPDIR)/$$i; ln -sfv ../dev/tools/Makefile.dir Makefile) \ done) @@ -42,14 +42,14 @@ quick: include Makefile -include $(TOPDIR)/dev/Makefile.common +include $(TOPDIR)/dev/tools/Makefile.common -# this file is better described in dev/Makefile.dir +# this file is better described in dev/tools/Makefile.dir include .depend.devel -#if dev/Makefile.local exists, it is included -ifneq ($(wildcard $(TOPDIR)/dev/Makefile.local),) -include $(TOPDIR)/dev/Makefile.local +#if dev/tools/Makefile.local exists, it is included +ifneq ($(wildcard $(TOPDIR)/dev/tools/Makefile.local),) +include $(TOPDIR)/dev/tools/Makefile.local endif @@ -71,4 +71,4 @@ usage:: vars: @(cd $(TOPDIR); \ echo export COQTOP=`pwd`/ ; \ - echo export COQBIN=`pwd`/bin/ )
\ No newline at end of file + echo export COQBIN=`pwd`/bin/ ) |