aboutsummaryrefslogtreecommitdiff
path: root/Makefile
diff options
context:
space:
mode:
authorherbelin2001-10-01 12:44:57 +0000
committerherbelin2001-10-01 12:44:57 +0000
commitbbd32b601943e8864ff3842a2ed2d7ba9d1ecea2 (patch)
treeaf1b008d8ec169cb4fa47ee2de833162db82bedc /Makefile
parentde4df15b3dc66cfad2364019a2b7485b313a89f5 (diff)
Incompatibilite camlp4 -pp et windows resolu a partir de camlp4 3.01.6
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2090 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile10
1 files changed, 0 insertions, 10 deletions
diff --git a/Makefile b/Makefile
index e90ad7fc44..6444d30d58 100644
--- a/Makefile
+++ b/Makefile
@@ -769,16 +769,6 @@ clean::
.ml4.cmo:
$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4DEPS) $<` -impl" -c -impl $<
-# Use these lines for Windows
-#.ml4.cmx:
-# $(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4DEPS) $<` -o $*.ppo -impl $<
-# $(OCAMLOPT) $(OPTFLAGS) -c -impl $*.ppo
-
-# Use these lines for Windows
-#.ml4.cmo:
-# $(CAMLP4O) $(CAMLP4EXTENDFLAGS) `$(CAMLP4DEPS) $<` -o $*.ppo -impl $<
-# $(OCAMLC) $(BYTEFLAGS) -c -impl $*.ppo
-
.v.vo:
$(COQTOP) -boot -$(BEST) $(COQINCLUDES) -compile $*