@@ -9,6 +9,7 @@ SCRIPT_DIR="$(cd "$(dirname "${BASH_SOURCE[0]}")" && pwd)"
99REPO_ROOT=" $( cd " $SCRIPT_DIR /.." && pwd) "
1010WORKSPACE_DIR=" $REPO_ROOT /workspace"
1111MAX_UMOUNT_PASSES=5
12+ FORCE_DELETE=false
1213
1314run_privileged () {
1415 if [[ " $EUID " -eq 0 ]]; then
@@ -49,9 +50,10 @@ try_unmount_once() {
4950}
5051
5152usage () {
52- echo " Usage: $0 [--workspace-dir DIR] [--max-umount-passes N] [-h|--help]"
53+ echo " Usage: $0 [--workspace-dir DIR] [--max-umount-passes N] [--force] [- h|--help]"
5354 echo " --workspace-dir DIR Override workspace directory (default: $WORKSPACE_DIR )"
5455 echo " --max-umount-passes N Number of unmount retry passes (default: $MAX_UMOUNT_PASSES )"
56+ echo " --force Allow deleting a non-default workspace path"
5557 echo " -h, --help Show this help message"
5658}
5759
@@ -75,6 +77,10 @@ while [[ $# -gt 0 ]]; do
7577 MAX_UMOUNT_PASSES=" $2 "
7678 shift 2
7779 ;;
80+ --force)
81+ FORCE_DELETE=true
82+ shift
83+ ;;
7884 -h|--help)
7985 usage
8086 exit 0
@@ -87,6 +93,21 @@ while [[ $# -gt 0 ]]; do
8793 esac
8894done
8995
96+ if ! WORKSPACE_DIR=" $( realpath -m " $WORKSPACE_DIR " 2> /dev/null) " ; then
97+ echo " Failed to resolve workspace directory path: $WORKSPACE_DIR "
98+ exit 1
99+ fi
100+
101+ if [[ " $WORKSPACE_DIR " == " /" ]]; then
102+ echo " Refusing to remove root directory"
103+ exit 1
104+ fi
105+
106+ if [[ " $WORKSPACE_DIR " != " $REPO_ROOT /workspace" && " $FORCE_DELETE " != true ]]; then
107+ echo " Refusing to remove non-default workspace directory without --force: $WORKSPACE_DIR "
108+ exit 1
109+ fi
110+
90111if [[ ! -d " $WORKSPACE_DIR " ]]; then
91112 echo " Workspace directory does not exist: $WORKSPACE_DIR "
92113 exit 0
0 commit comments