Commit a8a67a1f authored by POTTIER Francois's avatar POTTIER Francois

Change find-menhir.sh to use the uninstalled Menhir (if found)

rather than the Menhir in the PATH. This helps build the demos
while working.
parent b689d803
......@@ -8,13 +8,7 @@
# A normal user does not need this script. One can
# assume that Menhir has been installed.
# First attempt: find Menhir in the PATH.
if which menhir >/dev/null ; then
echo menhir
exit 0
fi
# Second attempt: find Menhir in the src directory
# First attempt: find Menhir in the src directory
# of the Menhir distribution.
# This loop assumes that we are somewhere within
# the Menhir distribution, so by going up, we will
......@@ -28,6 +22,12 @@ if ls $LOCAL >/dev/null 2>/dev/null ; then
exit 0
fi
# Second attempt: find Menhir in the PATH.
if which menhir >/dev/null ; then
echo menhir
exit 0
fi
echo Error: could not find Menhir.
exit 1
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