Delete workdir if it does not exist

benedikt-schesch · May 27, 2024 · 5f6eb24 · 5f6eb24
1 parent 9c65713
commit 5f6eb24
Showing 1 changed file with 5 additions and 3 deletions.
diff --git a/run.sh b/run.sh
@@ -124,9 +124,11 @@ if [ -d "repos" ]; then
     find "repos/locks" -name "*.lock" -delete
 fi
 
-# Delete .workdir
-chmod -R +w .workdir
-rm -rf .workdir
+# Check if .workdir exists and delete it
+if [ -d .workdir ]; then
+    chmod -R +w .workdir
+    rm -rf .workdir
+fi
 
 python3 src/python/delete_cache_placeholders.py \
     --cache_dir "$CACHE_DIR"