diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-09-07 22:27:56 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-09-07 22:27:56 +0000 |
| commit | 307d2e286444dc6430e23c599778b768134cbf97 (patch) | |
| tree | e78c2e0f74b5ebd39a4391ab571ef79275715318 /Makefile | |
| parent | f73034a0a11f5d4bb902e8ea07c8f5492148cc05 (diff) | |
Generalize usage of $(FIND_VCS_CLAUSE) and add debian to it
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11389 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 11 |
1 files changed, 9 insertions, 2 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) |