diff --git a/devel.sh b/devel.sh new file mode 100755 index 0000000..c00b479 --- /dev/null +++ b/devel.sh @@ -0,0 +1,27 @@ +#!/bin/sh +# +# Script to clone and start a development server + +set -e + +if [ -f tools/devel-server.py ]; then + cat <