Merge "No more undefined usage of rev{Start,End}Id warnings"

[lhc/web/wiklou.git] / maintenance / dev / install.sh

diff --git a/maintenance/dev/install.sh b/maintenance/dev/install.sh
index 067d687..2219894 100755 (executable)
--- a/maintenance/dev/install.sh
+++ b/maintenance/dev/install.sh
@@ -1,8 +1,8 @@
 #!/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
-$DEV/installmw.sh
-$DEV/start.sh
+"$DEV/installphp.sh"
+"$DEV/installmw.sh"
+"$DEV/start.sh"