From cbb0b027e8ad7d53b22418737001d8d5a3ca900e Mon Sep 17 00:00:00 2001 From: Andrea Casarin Date: Thu, 28 Apr 2022 12:57:54 +0200 Subject: [PATCH] Option to disable PCRE JIT --- bin/install | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/bin/install b/bin/install index a4b60c8..a6a2b47 100755 --- a/bin/install +++ b/bin/install @@ -171,6 +171,12 @@ construct_configure_options() { configure_options="$configure_options --with-pdo-pgsql" fi + if [ "${PHP_WITHOUT_PCRE_JIT:-no}" != "no" ]; then + configure_options="$configure_options" + else + configure_options="$configure_options --without-pcre-jit" + fi + echo "$configure_options" }