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:27:08 +0200 |
commit | 0703c1b47725b8f36142d61c9197981f7e9a9e85 (patch) | |
tree | e6f4f44caabe5dbb31cfd0e232d48349162933bd /Makefile.menhir | |
parent | e63908464a17f9cd70a41a534e8cc6ba930a9954 (diff) | |
download | ocaml-0703c1b47725b8f36142d61c9197981f7e9a9e85.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 'Makefile.menhir')
-rw-r--r-- | Makefile.menhir | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.menhir b/Makefile.menhir index e8bc88ec11..a27a7d2835 100644 --- a/Makefile.menhir +++ b/Makefile.menhir @@ -83,7 +83,7 @@ promote-menhir: parsing/parser.mly .PHONY: import-menhirLib import-menhirLib: mkdir -p boot/menhir - cp \ + mv \ $(addprefix `$(MENHIR) --suggest-menhirLib`/menhirLib.,ml mli) \ boot/menhir |