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