diff --git a/devel.sh b/devel.sh index 86675e9..d79d263 100755 --- a/devel.sh +++ b/devel.sh @@ -1,8 +1,10 @@ -#!/bin/bash -e +#!/bin/sh # # Script to clone and start a development server -if [[ -f tools/devel-server.py ]]; then +set -e + +if [ -f tools/devel-server.py ]; then cat <