maintenance/dev/installphp.sh

   1 #!/bin/bash
   2
   3 if [[ "x$BASH_SOURCE" == "x" ]]; then echo '$BASH_SOURCE not set'; exit 1; fi
   4 DEV=$(cd -P "$(dirname "${BASH_SOURCE[0]}" )" && pwd)
   5
   6 set -e # DO NOT USE PIPES unless this is rewritten
   7
   8 if [ -d $DEV/php ]; then
   9         echo "PHP is already installed"
  10         exit 1
  11 fi
  12
  13 TAR=php5.4-latest.tar.gz
  14 PHPURL=http://snaps.php.net/$TAR
  15
  16 cd $DEV
  17
  18 # Some debain-like systems bundle wget but not curl, some other systems
  19 # like os x bundle curl but not wget... use whatever is available
  20 echo -n "Downloading PHP 5.4"
  21 if command -v wget &>/dev/null; then
  22         echo "- using wget"
  23         wget $PHPURL
  24 elif command -v curl &>/dev/null; then
  25         echo "- using curl"
  26         curl -O $PHPURL
  27 else
  28         echo "- aborting"
  29         echo "Could not find curl or wget." >&2;
  30         exit 1;
  31 fi
  32
  33 echo "Extracting php 5.4"
  34 tar -xzf $TAR
  35
  36 cd php5.4-*/
  37
  38 echo "Configuring and installing php 5.4 in $IP/maintenance/dev/php/"
  39 ./configure --prefix=$DEV/php/
  40 make
  41 make install