From 1f2fd044d534b901a8453410037cb78db76495ce Mon Sep 17 00:00:00 2001
From: susurri <susurrus.silent@gmail.com>
Date: Mon, 30 Nov 2020 01:04:40 +0900
Subject: [PATCH] feat: make gmp flag configurable

---
 bin/install | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/bin/install b/bin/install
index f268fa5..5bfc9ed 100755
--- a/bin/install
+++ b/bin/install
@@ -90,7 +90,6 @@ construct_configure_options() {
     --with-xmlrpc \
     --with-zip \
     --with-zlib \
-    --without-gmp \
     --without-snmp"
 
   if [ "$PHP_CONFIGURE_OPTIONS" = "" ]; then
@@ -99,6 +98,12 @@ construct_configure_options() {
     local configure_options="$PHP_CONFIGURE_OPTIONS $global_config"
   fi
 
+  if [ "${PHP_WITH_GMP:-no}" != "no" ]; then
+    configure_options="$configure_options --with-gmp"
+  else
+    configure_options="$configure_options --without-gmp"
+  fi
+
   if [ "${PHP_WITHOUT_PEAR:-no}" != "no" ]; then
     configure_options="$configure_options --without-pear"
   else