diff options
| -rwxr-xr-x | src/etc/pre-push.sh | 14 |
1 files changed, 14 insertions, 0 deletions
diff --git a/src/etc/pre-push.sh b/src/etc/pre-push.sh index 6f86c7ab8a4..7bacc943f25 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" |