diff options
Diffstat (limited to 'ext/gmp/config.w32')
| -rw-r--r-- | ext/gmp/config.w32 | 14 |
1 files changed, 0 insertions, 14 deletions
diff --git a/ext/gmp/config.w32 b/ext/gmp/config.w32 deleted file mode 100644 index 2aff16b77b..0000000000 --- a/ext/gmp/config.w32 +++ /dev/null @@ -1,14 +0,0 @@ -// $Id$ -// vim:ft=javascript - -ARG_WITH("gmp", "Include GNU MP support.", "no"); - -if (PHP_GMP != "no") { - if (CHECK_LIB("libgmp_a.lib", "gmp", PHP_GMP) && - CHECK_HEADER_ADD_INCLUDE("gmp.h", "CFLAGS_GMP", PHP_GMP)) { - EXTENSION("gmp", "gmp.c"); - AC_DEFINE('HAVE_GMP', 1, 'GMP support'); - } else { - WARNING("GMP not enabled; libraries and headers not found"); - } -} |