diff options
author | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-02-08 08:29:12 +0000 |
---|---|---|
committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-02-08 08:29:12 +0000 |
commit | 6b2d99445d35ea71cd24becb7f936e0cc9779d46 (patch) | |
tree | d16266e4a50ca83c2629e9e011c4d85fd5390690 /Makefile | |
parent | cb2fff45e8a936b30ba1351f37b785f8f8ec8b98 (diff) |
simplification du make depend; fonctions de stat. util. memoire dans certains modules
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1355 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
-rw-r--r-- | Makefile | 24 |
1 files changed, 11 insertions, 13 deletions
@@ -634,32 +634,31 @@ cleanconfig:: # Dependencies ########################################################################### -alldepend: depend dependcoq dependcamlp4 - -depend: beforedepend - $(OCAMLDEP) $(DEPFLAGS) */*.mli */*/*.mli */*.ml */*/*.ml > .depend +alldepend: depend dependcoq dependcoq: beforedepend $(COQDEP) $(COQINCLUDES) */*.v */*/*.v > .depend.coq -# Dependency of camlp4 files: this is tricky. +# Computing the dependencies in camlp4 files is tricky. # We proceed in several steps: + ML4FILESML = $(ML4FILES:.ml4=.ml) -dependcamlp4: + +depend: beforedepend # 1. We express dependencies of the .ml files w.r.t their grammars - rm -f .depend.camlp4.2 + rm -f .depend.camlp4 for f in $(ML4FILES); do \ - printf "%s" `dirname $$f`/`basename $$f .ml4`".ml: " >> .depend.camlp4.2; \ - echo `$(CAMLP4DEPS) $$f` >> .depend.camlp4.2; \ + printf "%s" `dirname $$f`/`basename $$f .ml4`".ml: " >> .depend.camlp4; \ + echo `$(CAMLP4DEPS) $$f` >> .depend.camlp4; \ done # 2. Then we are able to produce the .ml files using Makefile.dep $(MAKE) -f Makefile.dep $(ML4FILESML) # 3. We compute the dependencies inside the .ml files using ocamldep - ocamldep $(DEPFLAGS) $(ML4FILESML) > .depend.camlp4 + $(OCAMLDEP) $(DEPFLAGS) */*.mli */*/*.mli */*.ml */*/*.ml > .depend # 4. We express dependencies of .cmo files w.r.t their grammars for f in $(ML4FILES); do \ - printf "%s" `dirname $$f`/`basename $$f .ml4`".cmo: " >> .depend.camlp4; \ - echo `$(CAMLP4DEPS) $$f` >> .depend.camlp4; \ + printf "%s" `dirname $$f`/`basename $$f .ml4`".cmo: " >> .depend; \ + echo `$(CAMLP4DEPS) $$f` >> .depend; \ done # 5. Finally, we erase the generated .ml files rm -f $(ML4FILESML) @@ -670,4 +669,3 @@ clean:: include .depend include .depend.coq -include .depend.camlp4 |