diff options
author | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-02-05 17:32:09 +0000 |
---|---|---|
committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-02-05 17:32:09 +0000 |
commit | c6dff86156115dba6e3d90ac9d23cb7ea7e702e9 (patch) | |
tree | 9e4e11785c2f4affec3f3a6747267dc552eac907 /Makefile.dep | |
parent | 8846e497d6f869191645e18a9e2a8dc68956d679 (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.dep | 8 |
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 $@ |