aboutsummaryrefslogtreecommitdiffhomepage
path: root/Makefile
diff options
context:
space:
mode:
Diffstat (limited to 'Makefile')
-rw-r--r--Makefile8
1 files changed, 3 insertions, 5 deletions
diff --git a/Makefile b/Makefile
index e688304e3..c74cf5eed 100644
--- a/Makefile
+++ b/Makefile
@@ -1396,21 +1396,19 @@ proofs/tacexpr.cmx: proofs/tacexpr.ml
$(SHOW)'OCAMLOPT -rectypes $<'
$(HIDE)$(OCAMLOPT) -rectypes $(OPTFLAGS) -c $<
-# files compiled with camlp4 because of macros
+ML4FILES += lib/pp.ml4 lib/compat.ml4
lib/compat.cmo: lib/compat.ml4
$(SHOW)'OCAMLC4 $<'
$(HIDE)$(OCAMLC) $(BYTEFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) -D$(CAMLVERSION) -impl" -c -impl $<
lib/compat.cmx: lib/compat.ml4
- $(SHOW)'OCAMLC $<'
+ $(SHOW)'OCAMLOPT $<'
$(HIDE)$(OCAMLOPT) $(OPTFLAGS) -pp "$(CAMLP4O) $(CAMLP4EXTENDFLAGS) -D$(CAMLVERSION) -impl" -c -impl $<
# files compiled with camlp4 because of streams syntax
-ML4FILES += lib/pp.ml4 \
- lib/compat.ml4 \
- contrib/xml/xml.ml4 \
+ML4FILES += contrib/xml/xml.ml4 \
contrib/xml/acic2Xml.ml4 \
contrib/xml/proofTree2Xml.ml4 \
contrib/interface/line_parser.ml4 \