diff options
| -rw-r--r-- | Makefile | 11 | ||||
| -rw-r--r-- | Makefile.build | 5 |
2 files changed, 12 insertions, 4 deletions
@@ -24,7 +24,14 @@ # by Emacs' next-error. ########################################################################### -FIND_VCS_CLAUSE:='(' -name '{arch}' -or -name '.svn' -or -name '_darcs' -or -name '.git' -or -name "$${GIT_DIR}" ')' -prune -or +FIND_VCS_CLAUSE:='(' \ + -name '{arch}' -or \ + -name '.svn' -or \ + -name '_darcs' -or \ + -name '.git' -or \ + -name 'debian' -or \ + -name "$${GIT_DIR}" \ +')' -prune -or FIND_PRINTF_P:=-print | sed 's|^\./||' export YACCFILES:=$(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.mly' ')' $(FIND_PRINTF_P)) @@ -43,7 +50,7 @@ export MLIFILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.mli' ')' $(FIN export ML4FILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.ml4' ')' $(FIND_PRINTF_P)) #export VFILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.v' ')' $(FIND_PRINTF_P)) \ # $(GENVFILES) -export CFILES := $(shell find kernel/byterun -name '*.c') +export CFILES := $(shell find kernel/byterun $(FIND_VCS_CLAUSE) -name '*.c') export ML4FILESML:= $(ML4FILES:.ml4=.ml) diff --git a/Makefile.build b/Makefile.build index 908c0a67cc..a159fc95f9 100644 --- a/Makefile.build +++ b/Makefile.build @@ -667,7 +667,7 @@ install-library: ifeq ($(BEST),opt) $(INSTALLLIB) $(LINKCMX) $(FULLCOQLIB) endif - find . -name \*.cmi -exec $(INSTALLLIB) {} $(FULLCOQLIB) \; + find . $(FIND_VCS_CLAUSE) -name \*.cmi -exec $(INSTALLLIB) {} $(FULLCOQLIB) \; # csdpcert is not meant to be directly called by the user; we install # it with libraries -$(MKDIR) -p $(FULLCOQLIB)/contrib/micromega @@ -715,7 +715,8 @@ install-latex: source-doc: if !(test -d $(SOURCEDOCDIR)); then mkdir $(SOURCEDOCDIR); fi - $(OCAMLDOC) -html -rectypes $(LOCALINCLUDES) -d $(SOURCEDOCDIR) `find . -name "*.ml"` + $(OCAMLDOC) -html -rectypes $(LOCALINCLUDES) -d $(SOURCEDOCDIR) \ + `find . $(FIND_VCS_CLAUSE) -name "*.ml"` ########################################################################### |