diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-03-04 20:12:07 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-03-04 20:12:07 +0000 |
| commit | 0bdb6949f88eb3493a39d6702179d0cfde74a25e (patch) | |
| tree | 688b6f3dbea7a1202889d18d7229adbb56d55f46 | |
| parent | 8ec7f7267d92cfc891a265c382e807bff5eefc40 (diff) | |
Makefile: a nicer hack concerning ocamlopt with no .mli: -intf-suffix .cmi (thanks A. Frisch)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12841 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | Makefile.build | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/Makefile.build b/Makefile.build index aec75d36f..73c3d371a 100644 --- a/Makefile.build +++ b/Makefile.build @@ -760,18 +760,19 @@ COND_OPTFLAGS= \ ## 1) We make .cmx always depend on .cmi ## 2) This .cmi will be created from the .mli, or trigger the compilation of the ## .cmo if there's no .mli (see rule below about MLWITHOUTMLI) -## 3) We tell ocamlopt to output to temporary names, remove the temp .cmi -## (since the actual .cmi should already be there and up-to-date) and move -## the temp .cmx and .o back in place +## 3) We tell ocamlopt to use the .cmi as the interface source file. With this +## hack, everything goes as if there is a .mli, and the .cmi is preserved +## and the .cmx is checked with respect to this .cmi -$(MLFILES:.ml=.cmx): %.cmx: %.cmi +HACKMLI = $(if $(wildcard $<i),,-intf-suffix .cmi) + +$(MLWITHOUTMLI:.ml=.cmx): %.cmx: %.cmi # for .ml with .mli this is already the case $(MLWITHOUTMLI:.ml=.cmi): %.cmi: %.cmo %.cmx: %.ml | %.ml.d $(SHOW)'OCAMLOPT $<' - $(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) -c -o $*.tmp.cmx $< && \ - rm -f $*.tmp.cmi && mv -f $*.tmp.o $*.o && mv -f $*.tmp.cmx $*.cmx + $(HIDE)$(OCAMLOPT) $(COND_OPTFLAGS) $(HACKMLI) -c $< %.cmxs: %.cmxa $(SHOW)'OCAMLOPT -shared -o $@' |