From 5f6eb2448d699e9a45eef2c3c606b9c1428e7214 Mon Sep 17 00:00:00 2001
From: Benedikt Schesch <b.schesch@gmail.com>
Date: Mon, 27 May 2024 13:46:01 -0700
Subject: [PATCH] Delete workdir if it does not exist

---
 run.sh | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/run.sh b/run.sh
index 0ff3955fc7..d1068170e9 100755
--- 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"