12345678910111213141516171819202122 |
- #!/usr/bin/env bash
- 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
- echo "servers.pid exists!"
- exit 1
- fi
- for port in 8080 8081 8082; do
- rm -rf "${DIR:?}/$port"
- rm -rf "$DIR/media_store.$port"
- done
- rm -rf "${DIR:?}/etc"
|