diff options
| author | Pierre Letouzey | 2017-06-15 15:24:03 +0200 |
|---|---|---|
| committer | Pierre Letouzey | 2017-06-15 15:35:03 +0200 |
| commit | d1d068bcc7ed43d375b1f69a3cc796fb12333519 (patch) | |
| tree | 15a2e1c82036d185880d124e5f93681b0b9d0a51 /dev | |
| parent | 28c732ea340f5ac571a77a8ac26de600c29165b2 (diff) | |
Makefile.build : restore (temporarily?) the anti-cmi-corruption hacks
Due to the recent conversion of many .mli-only files into .ml files
(hugely debatable impact of the API introduction), parallel make may
fail badly again (always the same race between ocamlc and ocamlopt for .cmi).
Still working on a proper fix, but meanwhile let's reintroduce the
old hacks against these corruptions.
Diffstat (limited to 'dev')
0 files changed, 0 insertions, 0 deletions