diff options
| author | Dan Callahan <danc@element.io> | 2021-10-27 21:36:18 +0100 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-10-27 21:36:18 +0100 |
| commit | a1ba7a850aaad51799ce77006ac5e8a425881765 (patch) | |
| tree | aa501e65702a3e3fb179c3a0c37dc15543637f72 /demo/clean.sh | |
| parent | Annotate `log_function` decorator (#10943) (diff) | |
| parent | Merge remote-tracking branch 'origin/develop' into shellcheck (diff) | |
| download | synapse-a1ba7a850aaad51799ce77006ac5e8a425881765.tar.xz | |
Update scripts to pass Shellcheck lints (#11166)
Diffstat (limited to 'demo/clean.sh')
| -rwxr-xr-x | demo/clean.sh | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/demo/clean.sh b/demo/clean.sh index 6b809f6e83..e9b440d90d 100755 --- a/demo/clean.sh +++ b/demo/clean.sh @@ -6,14 +6,14 @@ DIR="$( cd "$( dirname "$0" )" && pwd )" PID_FILE="$DIR/servers.pid" -if [ -f $PID_FILE ]; then +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 + rm -rf "${DIR:?}/$port" + rm -rf "$DIR/media_store.$port" done -rm -rf $DIR/etc +rm -rf "${DIR:?}/etc" |