summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMatthias Andreas Benkard <matthias@benkard.de>2008-08-20 13:08:39 +0200
committerMatthias Andreas Benkard <matthias@benkard.de>2008-08-20 13:08:39 +0200
commit597a22df04342e04051388564b86c649603727d9 (patch)
treebca8c35d7f6449cd051cda3ea853b494dd63360f
parenta1bd5fac22b51da3d0593de04e26c1215f6730e9 (diff)
configure: Check for GNU MP.
-rwxr-xr-xconfigure14
1 files changed, 14 insertions, 0 deletions
diff --git a/configure b/configure
index 39fe2a6..0fff95c 100755
--- a/configure
+++ b/configure
@@ -47,6 +47,9 @@ if ($? == 0) {
`echo '\#include <histedit.h>' | $CC $CFLAGS $OBJCFLAGS -c -o /dev/null -x c - 2>/dev/null`;
$histedit_h = 1 if ($? == 0);
+`echo '\#include <gmp.h>' | $CC $CFLAGS $OBJCFLAGS -c -o /dev/null -x c - 2>/dev/null`;
+$gmp_h = 1 if ($? == 0);
+
`$XCODEBUILD -version`;
if ($? == 0) {
$xcode = 1;
@@ -80,6 +83,17 @@ if ($no_ffi) {
}
}
+unless ($gmp_h) {
+ print " * GNU MP\n";
+ if ($darwin || $debian) {
+ $install = "$install gmp" if $darwin;
+ $install = "$install libgmp3-dev" if $debian;
+ $installp = 1;
+ } else {
+ push @steps, (" * Download and install GNU MP from: http://gmplib.org/\n");
+ }
+}
+
unless ($histedit_h) {
print " * libedit\n";
if ($darwin || $debian) {