From 3be19879b96d372c7f3c003b59863fb6358911c8 Mon Sep 17 00:00:00 2001
From: Aaron Muir Hamilton <aaron@correspondwith.me>
Date: Sat, 3 Feb 2018 22:17:37 +0000
Subject: [PATCH] dev.sh: Run `php` if there is no `php7.0` in PATH

---
 dev.sh | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/dev.sh b/dev.sh
index 22f09dbd..06fe5fb4 100755
--- a/dev.sh
+++ b/dev.sh
@@ -1,5 +1,7 @@
 #!/bin/bash
 
+PHPBIN=php7.0
+
 DIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
 
 
@@ -7,4 +9,8 @@ if [ ! -e "data/config.php" ]; then
   cp "$DIR/data/config.php.example" "$DIR/data/config.php"
 fi
 
-php7.0 --server localhost:8000 --docroot "$DIR/web" "$DIR/web/index.php"
+if ! which $PHPBIN 2>/dev/null; then
+    PHPBIN=php
+fi
+
+$PHPBIN --server localhost:8000 --docroot "$DIR/web" "$DIR/web/index.php"