aboutsummaryrefslogtreecommitdiffhomepage
path: root/configure
blob: 09585e59ee590469650956cd32b33019ace0ec27 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
#!/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