aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile
diff options
context:
space:
mode:
authorGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-02-08 08:29:12 +0000
committerGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-02-08 08:29:12 +0000
commit6b2d99445d35ea71cd24becb7f936e0cc9779d46 (patch)
treed16266e4a50ca83c2629e9e011c4d85fd5390690 /Makefile
parentcb2fff45e8a936b30ba1351f37b785f8f8ec8b98 (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--Makefile24
1 files changed, 11 insertions, 13 deletions
diff --git a/Makefile b/Makefile
index 33f4c1c8b..fae9c8d68 100644
--- a/Makefile
+++ b/Makefile
@@ -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