aboutsummaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
authormlasson2014-12-18 15:55:02 +0100
committerEnrico Tassi2014-12-18 17:08:07 +0100
commitfc3b70a11aff48eedd7b235f5732cd170a6ab8be (patch)
treee15dc7fb22e5491a991d2b5d4e13b52aa46dbf0b /tools
parent4cb94e38a29badc26abd888875a21569672838dd (diff)
Bug fix (coq_makefile): Adding unix.cma and threads.cma dependencies for grammar in campl4
Diffstat (limited to 'tools')
-rw-r--r--tools/coq_makefile.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index acef1e643a..c8087f7f10 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -454,11 +454,11 @@ let variables is_install opt (args,defs) =
print "CAMLOPTLINK?=$(OCAMLOPT) -rectypes -thread\n";
print "GRAMMARS?=grammar.cma\n";
print "ifeq ($(CAMLP4),camlp5)
-CAMLP4EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo
+CAMLP4EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo unix.cma threads.cma
else
CAMLP4EXTEND=
endif\n";
- print "PP?=-pp '$(CAMLP4O) -I $(CAMLLIB) $(COQSRCLIBS) compat5.cmo \\
+ print "PP?=-pp '$(CAMLP4O) -I $(CAMLLIB) -I $(CAMLLIB)threads/ $(COQSRCLIBS) compat5.cmo \\
$(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl'\n\n";
end;
match is_install with