Makefile.build: "make;make" should redo nothing

 As reported by PMP, this was not yet the case. The culprit
 was the build of coqdep_boot by a one-liner ocamlopt taking all
 the necessary .ml files as arguments (in the right order). This
 was nice and short, and correct wrt dependencies, but had the
 inconvenient of building some .cmi *after* their corresponding
 .cmx, while the rest of the Makefile relies on the reverse order
 (see the section about MLWITHOUTMLI). Hence on the next run,
 make was thinking that these .cmx weren't up-to-date.

 For solving this issue, we now build coqdep_boot (and other tools)
 via a list of .cmx and let our infractructure build them (after
 their .cmi). The only drawback is the 6 extra lines to hardcode
 the dependencies of the *.cm(o|i|x) needed for coqdep_boot.
 (since the .ml.d aren't already taken in account by make at that
 time).

0 files changed, 0 insertions, 0 deletions