diff options
author | Matthias Andreas Benkard <matthias@benkard.de> | 2008-08-20 13:08:39 +0200 |
---|---|---|
committer | Matthias Andreas Benkard <matthias@benkard.de> | 2008-08-20 13:08:39 +0200 |
commit | 597a22df04342e04051388564b86c649603727d9 (patch) | |
tree | bca8c35d7f6449cd051cda3ea853b494dd63360f | |
parent | a1bd5fac22b51da3d0593de04e26c1215f6730e9 (diff) |
configure: Check for GNU MP.
-rwxr-xr-x | configure | 14 |
1 files changed, 14 insertions, 0 deletions
@@ -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) { |