From 0197661f851bbe4ec7d6b189d41b45173daad968 Mon Sep 17 00:00:00 2001
From: Michele Locati <michele@locati.it>
Date: Thu, 5 May 2022 18:47:46 +0200
Subject: [PATCH] Fix installing excimer on PHP 7.1 (#570)

The issue has already been fixed by
https://gerrit.wikimedia.org/r/plugins/gitiles/mediawiki/php/excimer/+/aed4ff82438e05e8c744ec5a7a1aa892aa9ac6f7
but we need to wait for a new version

Test: excimer
---
 install-php-extensions | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/install-php-extensions b/install-php-extensions
index f75a9cd..ad1ec52 100755
--- a/install-php-extensions
+++ b/install-php-extensions
@@ -2509,6 +2509,13 @@ installRemoteModule() {
 			# event must be loaded after sockets
 			installRemoteModule_ini_basename="xx-php-ext-$installRemoteModule_module"
 			;;
+		excimer)
+			if test -z "$installRemoteModule_version"; then
+				if test $PHP_MAJMIN_VERSION -le 701; then
+					installRemoteModule_version=1.0.2
+				fi
+			fi
+			;;
 		gearman)
 			if test -z "$installRemoteModule_version"; then
 				if test $PHP_MAJMIN_VERSION -le 506; then