aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile.dep
diff options
context:
space:
mode:
authorGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-02-05 17:32:09 +0000
committerGravatar filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7>2001-02-05 17:32:09 +0000
commitc6dff86156115dba6e3d90ac9d23cb7ea7e702e9 (patch)
tree9e4e11785c2f4affec3f3a6747267dc552eac907 /Makefile.dep
parent8846e497d6f869191645e18a9e2a8dc68956d679 (diff)
calcul des dependances camlp4 et production directe ml4 -> cmo (avec Judicael)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1325 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile.dep')
-rw-r--r--Makefile.dep8
1 files changed, 8 insertions, 0 deletions
diff --git a/Makefile.dep b/Makefile.dep
new file mode 100644
index 000000000..18f4ae29f
--- /dev/null
+++ b/Makefile.dep
@@ -0,0 +1,8 @@
+
+# This Makefile is designed to make the .ml files corresponding to .ml4 files
+
+include Makefile
+include .depend.camlp4.2
+
+.ml4.ml:
+ $(CAMLP4O) $(CAMLP4EXTENDFLAGS) pr_o.cmo `$(CAMLP4DEPS) $<` -impl $< > $@ || rm -f $@