51023619cc5c2f61a92234af6c850457eab3c526
3 if [ "x$BASH_SOURCE" == "x" ]; then echo '$BASH_SOURCE not set'; exit 1; fi
4 DEV
=$
(cd -P "$(dirname "${BASH_SOURCE[0]}" )" && pwd)
6 set -e # DO NOT USE PIPES unless this is rewritten
8 if [ -d "$DEV/php" -a -x "$DEV/php/bin/php" ] ||
[ -d "$HOME/.mwphp" -a -x "$HOME/.mwphp/bin/php" ]; then
9 echo "PHP is already installed"
13 TAR
=php5.4
-latest.
tar.gz
14 PHPURL
="http://snaps.php.net/$TAR"
18 echo "Preparing to download and install a local copy of PHP 5.4, note that this can take some time to do."
19 echo "If you wish to avoid re-doing this for uture dev installations of MediaWiki we suggest installing php in ~/.mwphp"
20 echo -n "Install PHP in ~/.mwphp [y/N]: "
23 case "$INSTALLINHOME" in
32 # Some debain-like systems bundle wget but not curl, some other systems
33 # like os x bundle curl but not wget... use whatever is available
34 echo -n "Downloading PHP 5.4"
35 if command -v wget
&>/dev
/null
; then
38 elif command -v curl
&>/dev
/null
; then
43 echo "Could not find curl or wget." >&2;
47 echo "Extracting php 5.4"
52 echo "Configuring and installing php 5.4 in $PREFIX"
53 .
/configure
--prefix="$PREFIX"