If we failed to configure the GMP library and we are not using a system-wide one, abort.

This commit is contained in:
Juan Jose Garcia Ripoll 2010-03-06 21:08:36 +01:00
parent 530a3cefb4
commit 15a0668cd0
2 changed files with 8 additions and 0 deletions

5
src/configure vendored
View file

@ -5529,6 +5529,11 @@ $as_echo "$as_me: Configuring included GMP library:" >&6;}
--libdir=${destdir} --build=${gmp_build} --host=${host_alias} \
CFLAGS="$CFLAGS" LDFLAGS="$LDFLAGS" CPPFLAGS="$CPPFLAGS" CC="${CC} ${PICFLAG}" \
"$GMP_ABI" $with_gmp)
if test ! -f gmp/config.status; then
{ { $as_echo "$as_me:$LINENO: error: Failed to configure the GMP library." >&5
$as_echo "$as_me: error: Failed to configure the GMP library." >&2;}
{ (exit 1); exit 1; }; }
fi
fi
else
if test "x$ECL_GMP_HEADER" = "x"; then

View file

@ -395,6 +395,9 @@ else
--libdir=${destdir} --build=${gmp_build} --host=${host_alias} \
CFLAGS="$CFLAGS" LDFLAGS="$LDFLAGS" CPPFLAGS="$CPPFLAGS" CC="${CC} ${PICFLAG}" \
"$GMP_ABI" $with_gmp)
if test ! -f gmp/config.status; then
AC_MSG_ERROR([Failed to configure the GMP library.])
fi
fi
else
if test "x$ECL_GMP_HEADER" = "x"; then