From bc906f741474128d2727a42e2ea7cee906406c30 Mon Sep 17 00:00:00 2001
From: Shivam Mathur <shivam_jpr@hotmail.com>
Date: Sat, 1 May 2021 16:34:21 +0530
Subject: [PATCH] Use mirror for ppa:ondrej/php on Ubuntu 16.04

---
 src/scripts/linux.sh | 13 +++++++++----
 1 file changed, 9 insertions(+), 4 deletions(-)

diff --git a/src/scripts/linux.sh b/src/scripts/linux.sh
index 5cfc7abc..d63c7637 100644
--- a/src/scripts/linux.sh
+++ b/src/scripts/linux.sh
@@ -30,12 +30,17 @@ cleanup_lists() {
 # Function to add ppa:ondrej/php.
 add_ppa() {
   ppa=${1:-ondrej/php}
-  if ! apt-cache policy | grep -q "$ppa"; then
+  if [ "$DISTRIB_RELEASE" = "16.04" ] && [ "$ppa" = "ondrej/php" ]; then
+    LC_ALL=C.UTF-8 sudo apt-add-repository --remove ppa:"$ppa" -y || true
+    LC_ALL=C.UTF-8 sudo apt-add-repository http://setup-php.com/ondrej/php/ubuntu -y
+    sudo apt-key adv --keyserver keyserver.ubuntu.com --recv 4f4ea0aae5267a6c
+  elif ! apt-cache policy | grep -q "$ppa"; then
     cleanup_lists "$(dirname "$ppa")"
     LC_ALL=C.UTF-8 sudo apt-add-repository ppa:"$ppa" -y
-    if [ "$DISTRIB_RELEASE" = "16.04" ]; then
-      sudo "$debconf_fix" apt-get update
-    fi
+  fi
+
+  if [ "$DISTRIB_RELEASE" = "16.04" ]; then
+    sudo "$debconf_fix" apt-get update
   fi
 }