aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
diff options
context:
space:
mode:
authorGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-06-14 22:16:26 +0000
committerGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-06-14 22:16:26 +0000
commitbc892142df9facc8347a513ba15e74c8b7a36289 (patch)
treeba861340b0cf334055f9933f957574dcbc60621e /tools
parentf68aec200a61b112845de2febb996478909b3cff (diff)
coq_makefile fixup
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15438 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tools')
-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 d7e34e059..4734fa6e7 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -380,7 +380,7 @@ CAMLP4EXTEND=pa_extend.cmo q_MLast.cmo pa_macro.cmo
else
CAMLP4EXTEND=
endif\n";
- print "PP?=-pp \"$(CAMLP4BIN)$(CAMLP4O) -I $(CAMLLIB) -I . $(COQSRCLIBS) compat5.cmo \\
+ print "PP?=-pp \"$(CAMLP4O) -I $(CAMLLIB) -I . $(COQSRCLIBS) compat5.cmo \\
$(CAMLP4EXTEND) $(GRAMMARS) $(CAMLP4OPTIONS) -impl\"\n\n";
end;
match is_install with