diff options
Diffstat (limited to 'configure')
-rwxr-xr-x | configure | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/configure b/configure index a9ab15b387..ef446d599d 100755 --- a/configure +++ b/configure @@ -1495,7 +1495,7 @@ echo "configure:1495: checking version of $MAKEINFO" >&5 ac_prog_version=`$MAKEINFO --version 2>&1 | sed -n 's/^.*GNU texinfo.* \([0-9][0-9.]*\).*$/\1/p'` case $ac_prog_version in '') ac_prog_version="v. ?.??, bad"; ac_verc_fail=yes;; - 3.1[1-9] | 3.[2-9][0-9] | 1.6[89] | 1.7[0-9]) + 3.1[1-9] | 3.[2-9][0-9] | 4.* | 1.6[89] | 1.7[0-9]) ac_prog_version="$ac_prog_version, ok"; ac_verc_fail=no;; *) ac_prog_version="$ac_prog_version, bad"; ac_verc_fail=yes;; |