aboutsummaryrefslogtreecommitdiff
path: root/Makefile.stage2
diff options
context:
space:
mode:
authorlmamane2007-07-16 10:16:38 +0000
committerlmamane2007-07-16 10:16:38 +0000
commita964a7da07af0921ce173c4ef2f89fc80609366c (patch)
tree2f0a96c3c2198a7874cb340960e50783778977b8 /Makefile.stage2
parente45135c43acd75a604da1b3eb6c90c161d064400 (diff)
A cleaner solution to "make deletes .ml4.d files -> infinite loop" problem
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10010 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile.stage2')
-rw-r--r--Makefile.stage21
1 files changed, 1 insertions, 0 deletions
diff --git a/Makefile.stage2 b/Makefile.stage2
index 97a10118ee..6fe020be9f 100644
--- a/Makefile.stage2
+++ b/Makefile.stage2
@@ -9,6 +9,7 @@
include Makefile.stage1
-include $(ML4FILES:.ml4=.ml4.ml.d)
+.SECONDARY: $(ML4FILES:.ml4=.ml4.ml.d)
.PHONY: stage2
stage2: $(COQDEP)