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 9cc4b21277e..7a56401d7f2 100755 --- a/configure +++ b/configure @@ -2363,7 +2363,7 @@ if test "x$with_gmp$with_gmp_include$with_gmp_lib" = x && test -d ${srcdir}/gmp; have_gmp=yes fi -if test -d ${srcdir}/gcc && test "x$have_gmp" == xno; then +if test -d ${srcdir}/gcc && test "x$have_gmp" = xno; then have_gmp=yes saved_CFLAGS="$CFLAGS" CFLAGS="$CFLAGS $gmpinc" |