diff options
Diffstat (limited to 'dev/tools')
-rw-r--r-- | dev/tools/Makefile.common | 52 | ||||
-rw-r--r-- | dev/tools/Makefile.devel | 16 | ||||
-rw-r--r-- | dev/tools/Makefile.dir | 4 | ||||
-rw-r--r-- | dev/tools/Makefile.subdir | 4 |
4 files changed, 12 insertions, 64 deletions
diff --git a/dev/tools/Makefile.common b/dev/tools/Makefile.common index 1ff5cf799..e69de29bb 100644 --- a/dev/tools/Makefile.common +++ b/dev/tools/Makefile.common @@ -1,52 +0,0 @@ -# this Makefile contains goals common for directory and main devel makefiles - -ifndef TOPDIR -TOPDIR=.. -endif - -ifndef BASEDIR -BASEDIR= -endif - -# the following entries are used to make synchronize two source trees -# (on big computer and on a laptop for example) - -OTHER_FILE=$(TOPDIR)/dev/other -OTHER=$(shell cat $(OTHER_FILE)) - -# this is a directory of useful temporary things -WORKDIR=tmp - -ifneq (,$(findstring n,$(MAKEFLAGS))) -NFLAG=-n -else -NFLAG= -endif - -check_other: - +@(if [ "$(OTHER)" = "" ] ; then \ - echo You must put the ssh path to the other Coq source in $(OTHER_FILE) ; \ - echo For example: chrzaszc@ruta:coq/V7 ; \ - exit 1; \ - fi) - -get: check_other - +rsync -Cauvz $(NFLAG) $(OTHER)/ $(TOPDIR)/ - +@(if [ -d $(TOPDIR)/$(WORKDIR) ]; then \ - rsync -auvz $(NFLAG) $(OTHER)/tmp/ $(TOPDIR)/tmp/ ; \ - fi) - -put: check_other - +rsync -Cauvz $(NFLAG) $(TOPDIR)/ $(OTHER)/ - +@(if [ -d $(TOPDIR)/$(WORKDIR) ]; then \ - rsync -auvz $(NFLAG) $(TOPDIR)/tmp/ $(OTHER)/tmp/ ; \ - fi) - -sync: get put - - -conflicts: - cvs status | grep File | grep conflicts | less - -confl: conflicts - diff --git a/dev/tools/Makefile.devel b/dev/tools/Makefile.devel index f3abb62dd..8dcc70cf7 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/ ) 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 diff --git a/dev/tools/Makefile.subdir b/dev/tools/Makefile.subdir index ff1f30772..cb914bd12 100644 --- a/dev/tools/Makefile.subdir +++ b/dev/tools/Makefile.subdir @@ -1,7 +1,7 @@ # if you work in a sub/sub-rectory of Coq # you should make a link to that makefile -# ln -s ../../dev/Makefile.subdir Makefile -# in order to have all the facilities of dev/Makefile.dir +# ln -s ../../dev/tools/Makefile.subdir Makefile +# in order to have all the facilities of dev/tools/Makefile.dir TOPDIR=../.. include $(TOPDIR)/dev/tools/Makefile.dir |