[minor] Makefile.menhir
This fixes a problematic issue to a wrong Makefile.menhir that
was supposed to have been fixed by f10736b9e6
, but actually was not.
Apologies for the flawed commits and for the noise.
(This is the sort of horror sorry when the `mv`, which intended to move
temporary Menhir-produced files to `boot/`, was wrongly placed (by myself)
on the call to copy the runtime files from Menhir's installation directory
into `boot/`. As a result, running 'promote-menhir' would break your Menhir
install...)
master
parent
596b2b4869
commit
5aa6713a57
|
@ -84,7 +84,7 @@ promote-menhir: parsing/parser.mly
|
|||
.PHONY: import-menhirLib
|
||||
import-menhirLib:
|
||||
mkdir -p boot/menhir
|
||||
mv \
|
||||
cp \
|
||||
$(addprefix `$(MENHIR) --suggest-menhirLib`/menhirLib.,ml mli) \
|
||||
boot/menhir
|
||||
|
||||
|
|
Loading…
Reference in New Issue