diff options
| author | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-10-18 11:10:32 +0200 |
|---|---|---|
| committer | Bernhard Schommer <bernhardschommer@gmail.com> | 2016-10-18 11:10:32 +0200 |
| commit | ab6a906f09514d1ed81fb0970fb7151021407062 (patch) | |
| tree | 627bef91884922ca0eb040ad9101b9026e2b89be /configure | |
| parent | 22efd958aef1d4372a905158befa5394dec3c604 (diff) | |
| download | compcert-ab6a906f09514d1ed81fb0970fb7151021407062.tar.gz compcert-ab6a906f09514d1ed81fb0970fb7151021407062.zip | |
Query menhir for location of menhir lib in config.
Since the menhir version required supports the --suggest-menhirLib
flag we can query it already in the configure script simplifying
the Makefile.menhir
Diffstat (limited to 'configure')
| -rwxr-xr-x | configure | 4 |
1 files changed, 3 insertions, 1 deletions
@@ -404,8 +404,9 @@ echo "Testing Menhir... " | tr -d '\n' menhir_ver=`menhir --version 2>/dev/null | sed -n -e 's/^.*version \([0-9]*\).*$/\1/p'` case "$menhir_ver" in 20[0-9][0-9][0-9][0-9][0-9][0-9]) - if test "$menhir_ver" -ge $MENHIR_REQUIRED; then + if test "$menhir_ver" -ge $MENHIR_REQUIRED; then echo "version $menhir_ver -- good!" + menhir_includes="-I `menhir --suggest-menhirLib`" else echo "version $menhir_ver -- UNSUPPORTED" echo "Error: CompCert requires Menhir version $MENHIR_REQUIRED or later." @@ -478,6 +479,7 @@ BINDIR=$bindir LIBDIR=$libdir SHAREDIR=$sharedir OCAML_OPT_COMP=$ocaml_opt_comp +MENHIR_INCLUDES=$menhir_includes EOF if $merlin; then cat >> Makefile.config <<EOF |