Rollup merge of #137618 - yotamofek:pr/pre-push-hook, r=Mark-Simulacrum

Skip `tidy` in pre-push hook if the user is deleting a remote branch

It's kinda annoying when I'm trying to delete remote branches and that triggers `tidy`, so small fix to prevent that.
Hopefully this should be an acceptable amount of complexity to add to this shell script.

Author: matthiaskrgr

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"