diff options
| author |  notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-06-14 12:55:05 +0000 |
|---|---|---|
| committer | notin <notin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-06-14 12:55:05 +0000 |
| commit | 54286eace13cf1f0509e85ff6f47705e741c2b64 (patch) | |
| tree | 9d92f5f5a05cedcb13b6bded54ec5b069269403b /Makefile | |
| parent | 6ca79f35e39542ef7bfec09638f94687cba8a33e (diff) | |
Correction du bug sur make depend
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9889 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
| -rw-r--r-- | Makefile | 8 |
1 files changed, 5 insertions, 3 deletions
@@ -1780,9 +1780,9 @@ cleanconfig:: alldepend: depend dependcoq dependcoq: beforedepend - $(MAKE) .depend.coq + $(MAKE) MAKEDEPEND=1 .depend.coq -\.depend.coq: +.depend.coq: $(COQDEP) -coqlib . -R theories Coq -R contrib Coq $(COQINCLUDES) \ $(ALLFSETS:.vo=.v) $(ALLREALS:.vo=.v) $(ALLVO:.vo=.v) > .depend.coq @@ -1819,7 +1819,7 @@ ml4filesml: .depend.camlp4 $(MAKE) -f Makefile.dep $(ML4FILESML) \.depend: */*.mli */*/*.mli */*.ml */*/*.ml $(ML4FILES) kernel/byterun/*.c - $(MAKE) depend + $(MAKE) MAKEDEPEND=1 depend depend: beforedepend dependp4 ml4filesml # 1. We express dependencies of the .ml files w.r.t their grammars @@ -1853,8 +1853,10 @@ devel: $(MAKE) -f dev/Makefile.devel setup-devel $(MAKE) $(DEBUGPRINTERS) +ifndef MAKEDEPEND -include .depend -include .depend.coq +endif clean:: find . -name "\.#*" -exec rm -f {} \; |