summary refs log tree commit diff
path: root/demo/clean.sh
diff options
context:
space:
mode:
Diffstat (limited to 'demo/clean.sh')
-rwxr-xr-xdemo/clean.sh3
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