Commit 284ed1cd authored by POTTIER Francois's avatar POTTIER Francois
Browse files

New script, so as to allow compiling the demos

even Menhir has not been installed yet.
parent 8965fca8
# This script tries to find the Menhir executable.
# This is useful because we would like the demos
# to work regardless of whether Menhir has been
# installed already.
# 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
# Second 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
# end up at the root of the distribution.
while ! [ -d src ] ; do
cd ..
if ls $LOCAL >/dev/null 2>/dev/null ; then
echo `pwd`/$LOCAL
exit 0
echo Error: could not find Menhir.
exit 1
Supports Markdown
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