aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar mlasson <marc.lasson@gmail.com>2015-06-25 15:41:27 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2015-09-03 00:46:52 +0200
commit0f2d41755d99770c4576776462a4e433fb8f0a02 (patch)
tree1df5fbd0f37d559728482d676b1a5848bb09fcf5
parentae8f843303060e1db96f72b42d744b8b200b0968 (diff)
Missing argument "-c" for coqdep in coq_makefile
Prior to commit 964d1b70, the dependency files .mllib.d and .mlpack.d were generated by a call to coqdep using the argument -c (for ocaml code). While doing some finetuning of the generation of implicit rules, this commit removed (I think by mistake) this "-c". And without this -c argument coqdep output nothing on mllib files leading to incorrect linking of mllibs.
-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 71134c2d9..934a632dd 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";