diff options
| author | Pierre Boutillier | 2014-07-07 09:35:22 +0200 |
|---|---|---|
| committer | Pierre Boutillier | 2014-07-07 09:36:10 +0200 |
| commit | 20870c950ba3620755697010ffc49adb71cb4118 (patch) | |
| tree | 3d31400eb3e3ca5e849c58743c42c128a9995bce /tools | |
| parent | f7e7dcb3513329d82b21f224bb5c5acec445752e (diff) | |
Coq_makefile: fix cmx compilation when there are both ml and mllib
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coq_makefile.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index d20971aacb..a9f94fbb7a 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -355,16 +355,17 @@ 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 "$(filter $(CMXFILES),$(ML4FILES:.ml4=.cmx)): %.cmx: %.ml4\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n"; + print "$(filter-out $(MLPACKFILES:.mlpack=.cmx),$(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 "$(filter $(CMXFILES),$(MLFILES:.ml=.cmx)): %.cmx: %.ml\n\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; + print "$(filter-out $(MLPACKFILES:.mlpack=.cmx),$(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 *) - print "$(MLFILES:.ml=.cmxs) $(ML4FILES:.ml4=.cmxs) $(MLPACKFILES:.mlpack=.cmxs): %.cmxs: %.cmx\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $<\n\n"; + print "$(filter-out $(MLLIBFILES:.mllib=.cmxs),$(MLFILES:.ml=.cmxs) $(ML4FILES:.ml4=.cmxs) $(MLPACKFILES:.mlpack=.cmxs)): %.cmxs: %.cmx +\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $<\n\n"; print "$(MLLIBFILES:.mllib=.cmxs): %.cmxs: %.cmxa\n\t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -linkall -shared -o $@ $<\n\n" in let mllib_rules () = print "$(MLLIBFILES:.mllib=.cma): %.cma: | %.mllib\n\t$(CAMLLINK) $(ZDEBUG) $(ZFLAGS) -a -o $@ $^\n\n"; |