Makefile: try to avoid rare make failures related with make -j + ocamlopt + .cmi

 As said now in a comment of Makefile.build:

 NB: for the moment ocamlopt erases and recreates .cmi if there's no .mli around.
 This can lead to nasty things with make -j (e.g. another process accessing a
 partial .cmi). To avoid that:
  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

 Ok, this is quite a hack. I'll make a proper bug report to ocaml asap...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12837 85f007b7-540e-0410-9357-904b9bb8a0f7

0 files changed, 0 insertions, 0 deletions