diff options
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 ########################################################################### |