aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2015-03-30 10:41:32 +0200
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2015-03-30 11:14:19 +0200
commitc8c545713fa1e248a62fbd9905be56a5449b96a0 (patch)
tree3c265a95d5bbfd4e7fe5d1917f42d130996505ac
parent596a4a5251cc50f50bd6d25e36c81341bf65cfed (diff)
coq_makefile: fix compilation with camlp4
-rw-r--r--tools/coq_makefile.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 72735e900..0931fd550 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -463,7 +463,7 @@ let variables is_install opt (args,defs) =
print "ifeq ($(CAMLP4),camlp5)
CAMLP4EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo unix.cma threads.cma
else
-CAMLP4EXTEND=
+CAMLP4EXTEND=threads.cma
endif\n";
print "PP?=-pp '$(CAMLP4O) -I $(CAMLLIB) -I $(CAMLLIB)threads/ $(COQSRCLIBS) compat5.cmo \\
$(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'\n\n";