From f247f75d31a1939fc57be0aa05893f041c4dbfa5 Mon Sep 17 00:00:00 2001
From: ignoramous <ignoramous@users.noreply.github.com>
Date: Tue, 20 Feb 2024 17:49:08 +0530
Subject: [PATCH] run: ignore kill trap fails

---
 run | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/run b/run
index f2ea1f8c30..bee3764a36 100755
--- a/run
+++ b/run
@@ -40,7 +40,7 @@ cleanup() {
   jobs -p > jobfile
   j=$(cat jobfile)
   echo "kill... $j"
-  kill -INT $j
+  kill -INT $j || true
   # does not work... jobs -p | xargs -r kill -9
   rm jobfile
 }