diff options
| author | Pierre Letouzey | 2016-06-24 02:37:03 +0200 |
|---|---|---|
| committer | Pierre Letouzey | 2016-06-24 02:37:03 +0200 |
| commit | f062b07eea7d06c6a762402e81630b091211d1c6 (patch) | |
| tree | 7011f9d79736bec9c53e3873a9a759eadd0fd2f8 | |
| parent | c954bb5600e39f2cc19a96bcbb912ac694b3c16a (diff) | |
Makefile.build: mitigate potential issues with multiple creations of pack .cmi
| -rw-r--r-- | Makefile.build | 11 |
1 files changed, 8 insertions, 3 deletions
diff --git a/Makefile.build b/Makefile.build index b225140bd3..382370df9f 100644 --- a/Makefile.build +++ b/Makefile.build @@ -500,15 +500,20 @@ test-suite: world $(ALLSTDLIB).v $(SHOW)'OCAMLOPT -a -o $@' $(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -a -o $@ $(filter-out %.mllib, $^) -# For plugin packs : +# For plugin packs + +# Note: both ocamlc -pack and ocamlopt -pack will create the same .cmi, and there's +# apparently no way to avoid that (no -intf-suffix hack as below). +# We at least ensure that these two commands won't run at the same time, by a fake +# dependency from the packed .cmx to the packed .cmo. %.cmo: %.mlpack $(SHOW)'OCAMLC -pack -o $@' $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) -pack -o $@ $(filter-out %.mlpack, $^) -%.cmx: %.mlpack +%.cmx: %.mlpack %.cmo $(SHOW)'OCAMLOPT -pack -o $@' - $(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -pack -o $@ $(filter-out %.mlpack, $^) + $(HIDE)$(OCAMLOPT) $(MLINCLUDES) $(OPTFLAGS) -pack -o $@ $(filter-out %.mlpack %.cmo, $^) COND_BYTEFLAGS= \ $(if $(filter tools/fake_ide% tools/coq_makefile%,$<), -I ide,) $(MLINCLUDES) $(BYTEFLAGS) |