Commit fcde90fe authored by POTTIER Francois's avatar POTTIER Francois

GNUmakefile: added [pin] and [unpin] entries.

parent 68ba7eb4
......@@ -6,7 +6,7 @@
SHELL := bash
.PHONY: all test clean package check api export godi opam local unlocal
.PHONY: all test clean package check api export godi opam local unlocal pin unpin
# -------------------------------------------------------------------------
......@@ -263,3 +263,9 @@ local:
unlocal:
sudo PATH="$(PATH)" $(MAKE) -C $(PACKAGE) PREFIX=/usr/local USE_OCAMLFIND=true uninstall
pin:
opam pin add menhir `pwd` -k git
unpin:
opam pin remove menhir
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment