diff options
Diffstat (limited to 'demo/clean.sh')
-rwxr-xr-x | demo/clean.sh | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/demo/clean.sh b/demo/clean.sh index e9b440d90d..7f1e192021 100755 --- a/demo/clean.sh +++ b/demo/clean.sh @@ -4,6 +4,9 @@ set -e DIR="$( cd "$( dirname "$0" )" && pwd )" +# Ensure that the servers are stopped. +$DIR/stop.sh + PID_FILE="$DIR/servers.pid" if [ -f "$PID_FILE" ]; then |