diff options
| author |  glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-03 11:32:28 +0000 |
|---|---|---|
| committer | glondu <glondu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-03 11:32:28 +0000 |
| commit | 9af3e71899558b5e0ee10ccd9e597bee9a9821d2 (patch) | |
| tree | 2d360f5cfdf377224ac64fa6f3fa1d99d7327463 /tools/coq_makefile.ml4 | |
| parent | ea60a60b66de43b0c51580587582ad82f21ebfb4 (diff) | |
Add unix.cma on camlp4 command-line in coq_makefile (Closes: #2326)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13060 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools/coq_makefile.ml4')
| -rw-r--r-- | tools/coq_makefile.ml4 | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4 index 450796a53..20ec649f0 100644 --- a/tools/coq_makefile.ml4 +++ b/tools/coq_makefile.ml4 @@ -279,6 +279,7 @@ let variables defs = print "COQDOC:=$(COQBIN)coqdoc\n"; print "COQMKTOP:=$(COQBIN)coqmktop\n"; (* Caml executables and relative variables *) + printf "CAMLLIB:=$(shell $(CAMLBIN)%s -where)\n" best_ocamlc; printf "CAMLC:=$(CAMLBIN)%s -c -rectypes\n" best_ocamlc; printf "CAMLOPTC:=$(CAMLBIN)%s -c -rectypes\n" best_ocamlopt; printf "CAMLLINK:=$(CAMLBIN)%s -rectypes\n" best_ocamlc; @@ -287,7 +288,7 @@ let variables defs = print "CAMLP4EXTEND:=pa_extend.cmo pa_macro.cmo q_MLast.cmo\n"; print "CAMLP4OPTIONS:=\n"; List.iter var_aux defs; - print "PP:=-pp \"$(CAMLP4BIN)$(CAMLP4)o -I . $(COQSRCLIBS) $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl\"\n"; + print "PP:=-pp \"$(CAMLP4BIN)$(CAMLP4)o -I $(CAMLLIB) unix.cma -I . $(COQSRCLIBS) $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl\"\n"; print "\n" let parameters () = |