diff options
author | 2007-10-11 18:45:30 +0000 | |
---|---|---|
committer | 2007-10-11 18:45:30 +0000 | |
commit | 3b9e93568a189227fc54204335fdf283c4d2b33a (patch) | |
tree | d5722fa34ceaa422a35a0d8acdb54449b7beca3c /Makefile.common | |
parent | 0ff8e6a43c35c632292c6d9bf8c28ec6a3fc16e0 (diff) |
Allow a few build system optimisations/corner-cutting
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10218 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile.common')
-rw-r--r-- | Makefile.common | 21 |
1 files changed, 0 insertions, 21 deletions
diff --git a/Makefile.common b/Makefile.common index ba911adb0..99742b436 100644 --- a/Makefile.common +++ b/Makefile.common @@ -433,27 +433,6 @@ PRINTERSCMO:=\ toplevel/cerrors.cmo toplevel/vernacexpr.cmo toplevel/vernacinterp.cmo \ dev/top_printers.cmo -FIND_VCS_CLAUSE:='(' -name '{arch}' -or -name '.svn' -or -name '_darcs' -or -name '.git' -or -name "$${GIT_DIR}" ')' -prune -or -FIND_PRINTF_P:=-print | sed 's|^\./||' - -YACCFILES:=$(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.mly' ')' $(FIND_PRINTF_P)) -LEXFILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.mll' ')' $(FIND_PRINTF_P)) -GENMLFILES:=$(LEXFILES:.mll=.ml) $(YACCFILES:.mly=.ml) \ - scripts/tolink.ml kernel/copcodes.ml -GENMLIFILES:=$(YACCFILES:.mly=.mli) -GENHFILES:=kernel/byterun/coq_jumptbl.h -GENFILES:=$(GENMLFILES) $(GENMLIFILES) $(GENHFILES) -MLFILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.ml' ')' $(FIND_PRINTF_P) | \ - while read f; do if ! [ -e "$${f}4" ]; then echo "$$f"; fi; done) \ - $(GENMLFILES) -MLIFILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.mli' ')' $(FIND_PRINTF_P)) \ - $(GENMLIFILES) -ML4FILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.ml4' ')' $(FIND_PRINTF_P)) -VFILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.v' ')' $(FIND_PRINTF_P)) -CFILES := $(shell find kernel/byterun -name '*.c') - -ML4FILESML:= $(ML4FILES:.ml4=.ml) - ########################################################################### # vo files ########################################################################### |