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