aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorlmamane2007-07-15 20:59:42 +0000
committerlmamane2007-07-15 20:59:42 +0000
commita3c4febd0141b7283a03d643f06e1f8cd9750276 (patch)
tree721688f23d5180486aa98e7893cde49b68c2437e
parente8f786b4ef55aae4fc40c46f1b73c185ee0e5819 (diff)
Makefile: use CFLAGS for dependency generation of .c files
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10003 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r--Makefile.build2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.build b/Makefile.build
index b93abc7e31..7f79c60c97 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -855,7 +855,7 @@ endif
%.c.d: %.c
$(SHOW)'CCDEP $<'
- $(HIDE)$(CC) -MM $(CINCLUDES) $< > $@
+ $(HIDE)$(CC) -MM $(CFLAGS) $(CINCLUDES) $< > $@
.PRECIOUS: %.ml %.mli %.d %.ml4.d kernel/copcodes.ml