diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coq_makefile.ml4 | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4 index d65270f51f..a27efe7147 100644 --- a/tools/coq_makefile.ml4 +++ b/tools/coq_makefile.ml4 @@ -188,9 +188,9 @@ let variables l = printf "CAMLOPTLINK:=$(CAMLBIN)%s -rectypes\n" best_ocamlopt; print "GRAMMARS:=grammar.cma\n"; print "CAMLP4EXTEND:=pa_extend.cmo pa_macro.cmo q_MLast.cmo\n"; - print "CAMLP4OPTIONS=\n"; - print "PP:=-pp \"$(CAMLP4BIN)$(CAMLP4)o -I . $(COQSRCLIBS) $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl\"\n"; + print "CAMLP4OPTIONS:=\n"; var_aux l; + print "PP:=-pp \"$(CAMLP4BIN)$(CAMLP4)o -I . $(COQSRCLIBS) $(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl\"\n"; print "\n" let absolute_dir dir = |