aboutsummaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2015-09-06 13:23:28 +0200
committerPierre-Marie Pédrot2015-09-06 13:23:28 +0200
commitd8b245d688ff64d17acd9e7591daf6d63b4e54f7 (patch)
tree0e202d1f39e97844d94a873b30e4fb14fb481f84 /tools
parentc53f2f75375dfffd2f258c76f5b722d37ab0daf9 (diff)
parent5080991902a05ee720ab1d6fa1c9d592d3ffd36c (diff)
Merge branch 'v8.5'
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 e902370c35..4b92d57082 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -386,12 +386,12 @@ let implicit () =
print "$(MLLIBFILES:.mllib=.cma): %.cma: | %.mllib\n\t$(CAMLLINK) $(ZDEBUG) $(ZFLAGS) -a -o $@ $^\n\n";
print "$(MLLIBFILES:.mllib=.cmxa): %.cmxa: | %.mllib\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -a -o $@ $^\n\n";
print "$(addsuffix .d,$(MLLIBFILES)): %.mllib.d: %.mllib\n";
- print "\t$(COQDEP) $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
+ print "\t$(COQDEP) $(OCAMLLIBS) -c \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
let mlpack_rules () =
print "$(MLPACKFILES:.mlpack=.cmo): %.cmo: | %.mlpack\n\t$(CAMLLINK) $(ZDEBUG) $(ZFLAGS) -pack -o $@ $^\n\n";
print "$(MLPACKFILES:.mlpack=.cmx): %.cmx: | %.mlpack\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -pack -o $@ $^\n\n";
print "$(addsuffix .d,$(MLPACKFILES)): %.mlpack.d: %.mlpack\n";
- print "\t$(COQDEP) $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n";
+ print "\t$(COQDEP) $(OCAMLLIBS) -c \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n";
in
let v_rules () =
print "$(VOFILES): %.vo: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n";