From 41a7c8312d9b21bbf96da0d39b5650dde03ec7ef Mon Sep 17 00:00:00 2001
From: Yotam Ofek <yotam.ofek@gmail.com>
Date: Tue, 25 Feb 2025 13:08:59 +0000
Subject: [PATCH] Skip `tidy` in pre-push hook if the user is deleting a remote
 branch

---
 src/etc/pre-push.sh | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/src/etc/pre-push.sh b/src/etc/pre-push.sh
index 6f86c7ab8a448..7bacc943f258b 100755
--- a/src/etc/pre-push.sh
+++ b/src/etc/pre-push.sh
@@ -7,6 +7,20 @@
 
 set -Euo pipefail
 
+# Check if the push is doing anything other than deleting remote branches
+SKIP=true
+while read LOCAL_REF LOCAL_SHA REMOTE_REF REMOTE_SHA; do
+    if [[ "$LOCAL_REF" != "(delete)" || \
+          "$LOCAL_SHA" != "0000000000000000000000000000000000000000" ]]; then
+        SKIP=false
+    fi
+done
+
+if $SKIP; then
+    echo "Skipping tidy check for branch deletion"
+    exit 0
+fi
+
 ROOT_DIR="$(git rev-parse --show-toplevel)"
 
 echo "Running pre-push script $ROOT_DIR/x test tidy"