diff options
| author | Gabriel Scherer <gabriel.scherer@gmail.com> | 2018-09-07 13:27:08 +0200 |
|---|---|---|
| committer | Gabriel Scherer <gabriel.scherer@gmail.com> | 2018-09-07 13:33:42 +0200 |
| commit | 596b2b48697d58b7f36fdcedd989f586a6dfda48 (patch) | |
| tree | 8c8d26d77592e2c0a014971ceefe16eb66b67adb /stdlib/Compflags | |
| parent | f10736b9e6c8a89a5d1b6a5c5da88ed98e6638a2 (diff) | |
| download | ocaml-596b2b48697d58b7f36fdcedd989f586a6dfda48.tar.gz | |
[minor] Makefile.menhir bugfix for non-subsecond make systems
François Pottier reported that, on his mac machine,
"make promote-menhir; make world" fails: it seemed
that parsing/parser.ml, after being produced as a temporary
file by the promote-menhir target, is not refreshed using
the `parsing/parser.ml: boot/menhir/parser.ml` rule from
Makefile (which does the MenhirLib->CamlinternalMenhirlib renaming).
The issue comes down to the fact that while boot/menhir/parser.ml
is always younger than the parsing/parser.ml produced by promote,
the time difference is very small (parser.ml is copied in boot/
immediately after production), and macos doesn't record creation times
with enough precision to notice it.
This PR removes the temporary parsing/parser.ml created by Menhir
in the promote-menhir rule, so that this file is not seen anymore
by 'make world', and has to be properly reproduced from boot/.
Diffstat (limited to 'stdlib/Compflags')
0 files changed, 0 insertions, 0 deletions
