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