Add a tool to delete branches which have been merged to origin/master

(imported from commit 5fd2449126eb3f0df57af0472a14f6c94aaaac75)

tools/clean-branches

@@ -0,0 +1,49 @@
+#!/bin/bash -e
+
+# Deletes any local branches which are ancestors of origin/master,
+# and also any branches in origin which are ancestors of
+# origin/master and are named like $USER-*.
+
+push_args=''
+
+function is_merged {
+    ! git rev-list -n 1 origin/master.."$1" | grep -q .
+}
+
+function clean_ref {
+    ref="$1"
+    case "$ref" in
+        */master | */HEAD)
+            return
+            ;;
+
+        refs/heads/*)
+            if is_merged "$ref"; then
+                echo "Deleting local branch $(echo "$ref" | sed 's!^refs/heads/!!')"
+                git update-ref -d "$ref"
+            fi
+            ;;
+
+        refs/remotes/origin/$USER-*)
+            if is_merged "$ref"; then
+                remote_name="$(echo "$ref" | sed 's!^refs/remotes/origin/!!')"
+                echo "Deleting remote branch $remote_name"
+                # NB: this won't handle spaces in ref names
+                push_args="$push_args :$remote_name"
+            fi
+            ;;
+    esac
+}
+
+if [ "$(git symbolic-ref HEAD)" != 'refs/heads/master' ]; then
+    echo "Check out master before you run this script." >&2
+    exit 1
+fi
+
+git fetch --prune origin
+
+eval $(git for-each-ref --shell --format='clean_ref %(refname);')
+
+if [ -n "$push_args" ]; then
+    git push origin $push_args
+fi