#!/bin/bash -e # # Script to clone and start a development server if [[ -f tools/devel-server.py ]]; then cat <