summaryrefslogtreecommitdiff
path: root/Makefile.menhir
diff options
context:
space:
mode:
authorGabriel Scherer <gabriel.scherer@gmail.com>2018-09-07 13:27:08 +0200
committerGabriel Scherer <gabriel.scherer@gmail.com>2018-09-07 13:27:08 +0200
commit0703c1b47725b8f36142d61c9197981f7e9a9e85 (patch)
treee6f4f44caabe5dbb31cfd0e232d48349162933bd /Makefile.menhir
parente63908464a17f9cd70a41a534e8cc6ba930a9954 (diff)
downloadocaml-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.menhir2
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