From 5aa6713a57c49bdb61452f7baaa9bfd65845629d Mon Sep 17 00:00:00 2001
From: Gabriel Scherer <gabriel.scherer@gmail.com>
Date: Fri, 7 Sep 2018 23:06:10 +0200
Subject: [PATCH] [minor] Makefile.menhir

This fixes a problematic issue to a wrong Makefile.menhir that
was supposed to have been fixed by f10736b9e6c, 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...)
---
 Makefile.menhir | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Makefile.menhir b/Makefile.menhir
index a5fd1ed55..638117c44 100644
--- a/Makefile.menhir
+++ b/Makefile.menhir
@@ -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