Commit 96adc2a8 authored by POTTIER Francois's avatar POTTIER Francois

Make [make unlocal] work even if there is no $(PACKAGE) directory.

parent 2590fd54
......@@ -268,7 +268,7 @@ local:
sudo PATH="$(PATH)" $(MAKE) -C $(PACKAGE) PREFIX=/usr/local USE_OCAMLFIND=true install
unlocal:
sudo PATH="$(PATH)" $(MAKE) -C $(PACKAGE) PREFIX=/usr/local USE_OCAMLFIND=true uninstall
sudo PATH="$(PATH)" $(MAKE) -f Makefile PREFIX=/usr/local USE_OCAMLFIND=true uninstall
pin:
opam pin add menhir `pwd` -k git
......
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