From 799c75e3addfd16d10a9846b9324e0a13dd8978e Mon Sep 17 00:00:00 2001
From: Indra Gunawan <guind.online@gmail.com>
Date: Wed, 24 Apr 2024 01:08:52 +0800
Subject: [PATCH] make gmp flag configurable

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

diff --git a/bin/install b/bin/install
index c40be12..063b55a 100755
--- a/bin/install
+++ b/bin/install
@@ -159,6 +159,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