aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorletouzey2008-05-22 11:21:47 +0000
committerletouzey2008-05-22 11:21:47 +0000
commitc941fc98f9a707b2a81eb3a1b36d1f497632b04b (patch)
treea1424a564568e84d1752828281ce0b10d7be17ff
parentcf73432c0e850242c7918cc348388e5cde379a8f (diff)
Should fix the dependancy issue mentioned by J.Forest about NMake:
.v.d are created exactly for all $(VFILES), which was only a "find -name .v", so $(GENVFILES) should be added to $(VFILES) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10965 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--Makefile3
1 files changed, 2 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index 96f0394c81..8e992cf4e3 100644
--- a/Makefile
+++ b/Makefile
@@ -41,7 +41,8 @@ export MLFILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.ml' ')' $(FIN
export MLIFILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.mli' ')' $(FIND_PRINTF_P)) \
$(GENMLIFILES)
export ML4FILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.ml4' ')' $(FIND_PRINTF_P))
-export VFILES := $(shell find . $(FIND_VCS_CLAUSE) '(' -name '*.v' ')' $(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 ML4FILESML:= $(ML4FILES:.ml4=.ml)