From f03373cf1e6c436c7b4bfdbfecc95d44084d9dc4 Mon Sep 17 00:00:00 2001
From: Daniel Friesen <dantman@users.mediawiki.org>
Date: Sun, 6 Nov 2011 23:49:16 +0000
Subject: [PATCH] Allow for installation of php in ~/.mwphp and don't die if
 maintenance/dev/data already existsy

---
 maintenance/dev/install.sh    |  2 +-
 maintenance/dev/installmw.sh  | 15 ++++++++++++---
 maintenance/dev/installphp.sh | 24 +++++++++++++++++++-----
 maintenance/dev/start.sh      | 13 +++++++++++--
 4 files changed, 43 insertions(+), 11 deletions(-)

diff --git a/maintenance/dev/install.sh b/maintenance/dev/install.sh
index daa7888491..2219894d29 100755
--- a/maintenance/dev/install.sh
+++ b/maintenance/dev/install.sh
@@ -1,6 +1,6 @@
 #!/bin/bash
 
-if [[ "x$BASH_SOURCE" == "x" ]]; then echo '$BASH_SOURCE not set'; exit 1; fi
+if [ "x$BASH_SOURCE" == "x" ]; then echo '$BASH_SOURCE not set'; exit 1; fi
 DEV=$(cd -P "$(dirname "${BASH_SOURCE[0]}" )" && pwd)
 
 "$DEV/installphp.sh"
diff --git a/maintenance/dev/installmw.sh b/maintenance/dev/installmw.sh
index 5d2cd64eda..7e352b6109 100755
--- a/maintenance/dev/installmw.sh
+++ b/maintenance/dev/installmw.sh
@@ -1,16 +1,25 @@
 #!/bin/bash
 
-if [[ "x$BASH_SOURCE" == "x" ]]; then echo '$BASH_SOURCE not set'; exit 1; fi
+if [ "x$BASH_SOURCE" == "x" ]; then echo '$BASH_SOURCE not set'; exit 1; fi
 DEV=$(cd -P "$(dirname "${BASH_SOURCE[0]}" )" && pwd)
 
+if [ -d "$DEV/php" -a -x "$DEV/php/bin/php" ]; then
+	PHP="$DEV/php/bin/php"
+elif [ -d "$HOME/.mwphp" -a -x "$HOME/.mwphp/bin/php" ]; then
+	PHP="$HOME/.mwphp/bin/php"
+else
+	echo "Local copy of PHP is not installed"
+	echo 1
+fi
+
 set -e
 
 PORT=4881
 
 cd "$DEV/../../"; # $IP
 
-mkdir "$DEV/data"
-"$DEV/php/bin/php" maintenance/install.php --server="http://localhost:$PORT" --scriptpath="" --dbtype=sqlite --dbpath="$DEV/data" --pass=admin "Trunk Test" "$USER"
+mkdir -p "$DEV/data"
+"$PHP" maintenance/install.php --server="http://localhost:$PORT" --scriptpath="" --dbtype=sqlite --dbpath="$DEV/data" --pass=admin "Trunk Test" "$USER"
 echo ""
 echo "Development wiki created with admin user $USER and password 'admin'."
 echo ""
diff --git a/maintenance/dev/installphp.sh b/maintenance/dev/installphp.sh
index b3285f3214..51023619cc 100755
--- a/maintenance/dev/installphp.sh
+++ b/maintenance/dev/installphp.sh
@@ -1,13 +1,13 @@
 #!/bin/bash
 
-if [[ "x$BASH_SOURCE" == "x" ]]; then echo '$BASH_SOURCE not set'; exit 1; fi
+if [ "x$BASH_SOURCE" == "x" ]; then echo '$BASH_SOURCE not set'; exit 1; fi
 DEV=$(cd -P "$(dirname "${BASH_SOURCE[0]}" )" && pwd)
 
 set -e # DO NOT USE PIPES unless this is rewritten
 
-if [ -d "$DEV/php" ]; then
+if [ -d "$DEV/php" -a -x "$DEV/php/bin/php" ] || [ -d "$HOME/.mwphp" -a -x "$HOME/.mwphp/bin/php" ]; then
 	echo "PHP is already installed"
-	exit 1
+	exit 0
 fi
 
 TAR=php5.4-latest.tar.gz
@@ -15,6 +15,20 @@ PHPURL="http://snaps.php.net/$TAR"
 
 cd "$DEV"
 
+echo "Preparing to download and install a local copy of PHP 5.4, note that this can take some time to do."
+echo "If you wish to avoid re-doing this for uture dev installations of MediaWiki we suggest installing php in ~/.mwphp"
+echo -n "Install PHP in ~/.mwphp [y/N]: "
+read INSTALLINHOME
+
+case "$INSTALLINHOME" in
+	[Yy] | [Yy][Ee][Ss] )
+		PREFIX="$HOME/.mwphp"
+		;;
+	*)
+		PREFIX="$DEV/php/"
+		;;
+esac
+
 # Some debain-like systems bundle wget but not curl, some other systems
 # like os x bundle curl but not wget... use whatever is available
 echo -n "Downloading PHP 5.4"
@@ -35,7 +49,7 @@ tar -xzf "$TAR"
 
 cd php5.4-*/
 
-echo "Configuring and installing php 5.4 in \$IP/maintenance/dev/php/"
-./configure --prefix="$DEV/php/"
+echo "Configuring and installing php 5.4 in $PREFIX"
+./configure --prefix="$PREFIX"
 make
 make install
diff --git a/maintenance/dev/start.sh b/maintenance/dev/start.sh
index 8904556673..3a0aa7e949 100755
--- a/maintenance/dev/start.sh
+++ b/maintenance/dev/start.sh
@@ -1,12 +1,21 @@
 #!/bin/bash
 
-if [[ "x$BASH_SOURCE" == "x" ]]; then echo '$BASH_SOURCE not set'; exit 1; fi
+if [ "x$BASH_SOURCE" == "x" ]; then echo '$BASH_SOURCE not set'; exit 1; fi
 DEV=$(cd -P "$(dirname "${BASH_SOURCE[0]}" )" && pwd)
 
+if [ -d "$DEV/php" -a -x "$DEV/php/bin/php" ]; then
+	PHP="$DEV/php/bin/php"
+elif [ -d "$HOME/.mwphp" -a -x "$HOME/.mwphp/bin/php" ]; then
+	PHP="$HOME/.mwphp/bin/php"
+else
+	echo "Local copy of PHP is not installed"
+	echo 1
+fi
+
 PORT=4881
 
 echo "Starting up MediaWiki at http://localhost:$PORT/"
 echo ""
 
 cd "$DEV/../../"; # $IP
-"$DEV/php/bin/php" -S "localhost:$PORT"
+"$PHP" -S "localhost:$PORT"
-- 
2.20.1