diff options
| author |  Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
|---|---|---|
| committer | Samuel Mimram <smimram@debian.org> | 2006-11-21 21:38:49 +0000 |
| commit | 208a0f7bfa5249f9795e6e225f309cbe715c0fad (patch) | |
| tree | 591e9e512063e34099782e2518573f15ffeac003 /dev/tools/Makefile.devel | |
| parent | de0085539583f59dc7c4bf4e272e18711d565466 (diff) | |
Imported Upstream version 8.1~gammaupstream/8.1.gamma
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 f3abb62d..8dcc70cf 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/ ) |