Skip to content

Commit

Permalink
Create [make demote-menhir] to undo the effect of [make promote-menhir].
Browse files Browse the repository at this point in the history
  • Loading branch information
fpottier committed Nov 20, 2018
1 parent f27c1de commit de3dcf1
Showing 1 changed file with 12 additions and 0 deletions.
12 changes: 12 additions & 0 deletions Makefile.menhir
Original file line number Diff line number Diff line change
Expand Up @@ -24,6 +24,10 @@
# updated result. Use it to make permanent changes to the compiler
# parser.
#
# - demote-menhir undoes the effect of promote-menhir. The files in
# the boot/ directory that are affected by promote-menhir and are
# under version control are restored to their normal state (HEAD).
#
# - test-menhir builds the parser from parser.mly without storing it
# in the boot/ directory, and only checks that the generated parser
# builds correctly. Use it to quickly check if a parser.mly change
Expand Down Expand Up @@ -89,6 +93,14 @@ import-menhirLib:
boot/menhir


## demote-menhir

DEMOTE:=menhirLib.ml menhirLib.mli parser.ml parser.mli

.PHONY: demote-menhir
demote-menhir:
git checkout HEAD -- $(addprefix boot/menhir/,$(DEMOTE))

## test-menhir

# This rule assumes that the `parsing/` sources and its dependencies
Expand Down

0 comments on commit de3dcf1

Please sign in to comment.