diff options
Diffstat (limited to 'configure')
-rwxr-xr-x | configure | 5 |
1 files changed, 3 insertions, 2 deletions
@@ -555,12 +555,13 @@ fi MENHIR_REQUIRED=20161201 MENHIR_NEW_API=20180530 +MENHIR_MAX=20181026 menhir_flags='' 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 -a "$menhir_ver" -le $MENHIR_MAX; then echo "version $menhir_ver -- good!" menhir_includes="-I `menhir --suggest-menhirLib`" if test "$menhir_ver" -ge $MENHIR_NEW_API; then @@ -568,7 +569,7 @@ case "$menhir_ver" in fi else echo "version $menhir_ver -- UNSUPPORTED" - echo "Error: CompCert requires Menhir version $MENHIR_REQUIRED or later." + echo "Error: CompCert requires a version of Menhir between $MENHIR_REQUIRED and $MENHIR_MAX, included." missingtools=true fi;; *) |