From 1076847767f08361efda20933fa9e3f79974297e Mon Sep 17 00:00:00 2001
From: lmamane
Date: Tue, 17 Jul 2007 22:24:33 +0000
Subject: Makefile: Do _not_ delete dummy .ml files of .ml4 files even when not
 needed anymore.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10015 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 Makefile.build | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/Makefile.build b/Makefile.build
index 7ef5f5a5cd..ad14d20984 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -845,7 +845,12 @@ endif
 	$(SHOW)'CCDEP     $<'
 	$(HIDE)$(CC) -MM -MQ "$@" -MQ "$(<:.c=.o)" $(CFLAGS) $(CINCLUDES) $< > $@
 
-.SECONDARY: $(GENFILES)
+## The GENFILES and ML4FILESML files need to be secondary, else they
+## get deleted by make after the dependencies get generated. This may
+## at first sight be a good thing, but then if any one .ml.d
+## dependency needs to be regenerated, these files get regenerated,
+## which triggers the recalculation of _all_ .ml.d dependencies!
+.SECONDARY: $(GENFILES) $(ML4FILESML)
 
 ###########################################################################
 # this sets up developper supporting stuff
-- 
cgit v1.2.3