diff options
| -rw-r--r-- | Makefile.menhir | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/Makefile.menhir b/Makefile.menhir index a5fd1ed551..a27a7d2835 100644 --- a/Makefile.menhir +++ b/Makefile.menhir @@ -72,7 +72,6 @@ promote-menhir: parsing/parser.mly 's,^#\(.*\)"[^"]*/menhir/standard.mly",#\1"menhir/standard.mly",g' \ parsing/$$f \ > boot/menhir/$$f; \ - rm parsing/$$f; \ done # The import-menhirLib invocation in promote-menhir ensures that each |