push-to-pull-request: Add --merge option.

Signed-off-by: Anders Kaseorg <anders@zulip.com>

tools/push-to-pull-request

@@ -13,6 +13,8 @@ GitHub to see the subsequent push to master as representing a
 merge of the PR, rather than requiring the PR to be manually
 (and to the casual observer misleadingly) closed instead.
 
+With --merge, also go ahead and merge the PR.
+
 REMOTE defaults to the value of the Git config variable
 \`zulip.zulipRemote\` if set, else to \`upstream\`.
 
@@ -24,15 +26,21 @@ See also \`reset-to-pull-request\`.
 EOF
 }
 
-args="$(getopt -o '' --long help -n "$0" -- "$@")"
+args="$(getopt -o '' --long help,merge -n "$0" -- "$@")"
 eval "set -- $args"
 
+merge=
+
 while true; do
     case "$1" in
         --help)
             usage
             exit 0
             ;;
+        --merge)
+            merge=t
+            shift
+            ;;
         --)
             shift
             break
@@ -107,6 +115,15 @@ if [ "$(pr_jq .maintainer_can_modify)" != "true" ]; then
     exit 1
 fi
 
+if [ "$merge" ]; then
+    pr_base_ref="$(pr_jq -r .base.ref)"
+    git fetch -- "$remote"
+    if ! git merge-base --is-ancestor -- "$remote/$pr_base_ref" @; then
+        echo "error: You need to rebase on $remote/$pr_base_ref first" >&2
+        exit 1
+    fi
+fi
+
 pr_head_repo_fq="$(pr_jq -r .head.repo.full_name)"
 pr_head_refname="$(pr_jq -r .head.ref)"
 
@@ -123,3 +140,7 @@ if [ -n "$tracking_ref" ]; then
     set -x
     git update-ref "$tracking_ref" @
 fi
+
+if [ "$merge" ]; then
+    git push -- "$remote" "@:$pr_base_ref"
+fi