diff options
| author | Pierre Letouzey | 2016-06-02 04:36:10 +0200 |
|---|---|---|
| committer | Pierre Letouzey | 2016-06-07 16:16:46 +0200 |
| commit | af6b36dd24651f1324e7babb982a345fde7d4b58 (patch) | |
| tree | 655421d94101b481f302cd7b17e0b6545cb2a00f | |
| parent | 8df8bc8e3e2aa67f02a83db02fbbe877fa0b0450 (diff) | |
coq_makefile: add some -ml-synonym to the ocamldep rules
Without this, dependencies upon a .ml4 (or a .mlpack) won't be handled
correctly.
| -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 7b76514e46..3a85d11332 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -381,19 +381,19 @@ let implicit () = let mli_rules () = print "$(MLIFILES:.mli=.cmi): %.cmi: %.mli\n\t$(CAMLC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; print "$(addsuffix .d,$(MLIFILES)): %.mli.d: %.mli\n"; - print "\t$(OCAMLFIND) ocamldep -slash $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in + print "\t$(CAMLDEP) $(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-out $(addsuffix .cmx,$(foreach lib,$(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(ML4FILES:.ml4=.cmx)): %.cmx: %.ml4\n"; print "\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $(PP) -impl $<\n\n"; print "$(addsuffix .d,$(ML4FILES)): %.ml4.d: %.ml4\n"; - print "\t$(OCAMLFIND) ocamldep -slash $(OCAMLLIBS) $(PP) -impl \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in + print "\t$(CAMLDEP) $(OCAMLLIBS) $(PP) -impl \"$<\" > \"$@\" || ( 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-out $(addsuffix .cmx,$(foreach lib,$(MLPACKFILES:.mlpack=_MLPACK_DEPENDENCIES),$($(lib)))),$(MLFILES:.ml=.cmx)): %.cmx: %.ml\n"; print "\t$(CAMLOPTC) $(ZDEBUG) $(ZFLAGS) $<\n\n"; print "$(addsuffix .d,$(MLFILES)): %.ml.d: %.ml\n"; - print "\t$(OCAMLFIND) ocamldep -slash $(OCAMLLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n" in + print "\t$(CAMLDEP) $(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 "$(filter-out $(MLLIBFILES:.mllib=.cmxs),$(MLFILES:.ml=.cmxs) $(ML4FILES:.ml4=.cmxs) $(MLPACKFILES:.mlpack=.cmxs)): %.cmxs: %.cmx \t$(CAMLOPTLINK) $(ZDEBUG) $(ZFLAGS) -shared -o $@ $<\n\n"; @@ -471,6 +471,7 @@ let variables is_install opt (args,defs) = print "CAMLOPTC?=$(OCAMLFIND) opt -c -rectypes -thread\n"; print "CAMLLINK?=$(OCAMLFIND) ocamlc -rectypes -thread\n"; print "CAMLOPTLINK?=$(OCAMLFIND) opt -rectypes -thread\n"; + print "CAMLDEP?=$(OCAMLFIND) ocamldep -slash -ml-synonym .ml4 -ml-synonym .mlpack\n"; print "CAMLLIB?=$(shell $(OCAMLFIND) printconf stdlib)\n"; print "GRAMMARS?=grammar.cma\n"; print "ifeq ($(CAMLP4),camlp5) |