aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coq_makefile.ml
diff options
context:
space:
mode:
authorGravatar Pierre Boutillier <pierre.boutillier@ens-lyon.org>2014-07-03 18:00:47 +0200
committerGravatar Pierre Boutillier <pierre.boutillier@ens-lyon.org>2014-07-03 18:19:09 +0200
commitf2327aa3c69f1695f99e2ccbfe00c4e54e56e7d2 (patch)
treea618bf2436a9e35785ce51c0f48986aaf308822c /tools/coq_makefile.ml
parent157ccc2da0f62dad730f1f13b875c48e3af4eb09 (diff)
Fix Coq_makefile in presence of mlpack
Diffstat (limited to 'tools/coq_makefile.ml')
-rw-r--r--tools/coq_makefile.ml6
1 files changed, 3 insertions, 3 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index 665a7a502..d20971aac 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -355,12 +355,12 @@ let implicit () =
print "\t$(OCAMLDEP) -slash $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
let ml4_rules () =
print "$(ML4FILES:.ml4=.cmo): %.cmo: %.ml4\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n";
- print "$(ML4FILES:.ml4=.cmx): %.cmx: %.ml4\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n";
+ print "$(filter $(CMXFILES),$(ML4FILES:.ml4=.cmx)): %.cmx: %.ml4\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n";
print "$(addsuffix .d,$(ML4FILES)): %.ml4.d: %.ml4\n";
print "\t$(COQDEP) $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
let ml_rules () =
print "$(MLFILES:.ml=.cmo): %.cmo: %.ml\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n";
- print "$(MLFILES:.ml=.cmx): %.cmx: %.ml\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $<\n\n";
+ print "$(filter $(CMXFILES),$(MLFILES:.ml=.cmx)): %.cmx: %.ml\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $<\n\n";
print "$(addsuffix .d,$(MLFILES)): %.ml.d: %.ml\n";
print "\t$(OCAMLDEP) -slash $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in
let cmxs_rules () = (* order is important here when there is foo.ml and foo.mllib *)
@@ -373,7 +373,7 @@ let implicit () =
print "\t$(COQDEP) $(OCAMLLIBS) \"$<\" > \"$@\" || ( 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 "$(MLIFILES:.mlpack=.cmx): %.cmx: | %.mlpack\n\t$(CAMLOPTLINK) $(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";
in