Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Fetching contributors…

Cannot retrieve contributors at this time

executable file 38 lines (28 sloc) 0.932 kb
#!/bin/sh
## This micro-configure shell script is here only to
## launch the real configuration via ocaml
cmd=ocaml
script=./configure.ml
if [ ! -f $script ]; then
echo "Error: file $script not found in the current directory."
echo "Please run the configure script from the root of the coq sources."
echo "Configuration script failed!"
exit 1
fi
## Parse the args, only looking for -camldir
## We avoid using shift to keep "$@" intact
last=
for i; do
case $last in
-camldir|--camldir) cmd="$i/ocaml"; break;;
esac
last=$i
done
## We check that $cmd is ok before the real exec $cmd
`$cmd -version > /dev/null 2>&1` && exec $cmd $script "$@"
## If we're still here, something is wrong with $cmd
echo "Error: failed to run $cmd"
echo "Please use the option -camldir <dir> if 'ocaml' is installed"
echo "in directory <dir>, or add <dir> to your path."
echo "Configuration script failed!"
exit 1
Jump to Line
Something went wrong with that request. Please try again.