tools: Add push-to-pull-request tool.

I've often done this by hand -- basically typed out the last line,
with the variables found from looking at the PR page in a browser.
Seems nicer for both us maintainers and the contributor, in particular
because the PR gets marked as merged, instead of closed.  But it's a
bit of a pain, and I do it maybe half the time or less; plus it's kind
of a subtle GitHub feature, and as a result I think other maintainers
of Zulip repos do this approximately never.

I've always figured this couldn't be hard to automate; today I decided
to take the 45 minutes to look up how, write out the script, QA it,
write up a nice usage message and some comments, and commit it. :)

tools/push-to-pull-request

@@ -0,0 +1,66 @@
+#!/bin/bash
+set -e
+
+usage () {
+    cat >&2 <<EOF
+usage: $0 PULL_REQUEST_ID [REMOTE]
+
+Force-push our HEAD to the given GitHub pull request branch.
+
+Useful for a maintainer to run just before pushing to master,
+after tweaking the branch and/or rebasing to latest.  This causes
+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.
+
+See also \`reset-to-pull-request\`.
+EOF
+    exit 1
+}
+
+pr_id="$1"
+remote="${2:-upstream}"
+
+if [ -z "$pr_id" ]; then
+    usage
+fi
+
+remote_url="$(git config remote."$remote".url)"
+repo_fq="$(echo "$remote_url" | perl -lne 'print $1 if (
+    m, ^ git\@github\.com:
+         ([^/]+ / [^/]+)
+         (?:\.git)?
+       $ ,x )')"
+
+if [ -z "$repo_fq" ]; then
+    # We're pretty specific about what we expect the URL to look like;
+    # there are probably more cases we could legitimately cover, which
+    # we can add if/when they come up for someone.
+    echo "error: couldn't parse remote URL as GitHub repo" >&2
+    exit 1
+fi
+
+# See https://developer.github.com/v3/pulls/#get-a-single-pull-request .
+# This is the old REST API; the new GraphQL API does look neat, but it
+# seems to require authentication even for simple lookups of public data,
+# and that'd be a pain for a simple script like this.
+pr_details="$(curl -s https://api.github.com/repos/"$repo_fq"/pulls/"$pr_id")"
+
+pr_jq () {
+    echo "$pr_details" | jq "$@"
+}
+
+if [ "$(pr_jq .maintainer_can_modify)" != "true" ]; then
+    # This seems to be rare (in Greg's experience doing the manual
+    # equivalent of this script for many different contributors, none
+    # have ever chosen this setting), but give a decent error message
+    # if it does happen.
+    echo "error: contributor has disallowed pushing to PR branch" >&2
+    exit 1
+fi
+
+pr_head_repo_fq="$(pr_jq -r .head.repo.full_name)"
+pr_head_refname="$(pr_jq -r .head.ref)"
+
+set -x
+exec git push git@github.com:"$pr_head_repo_fq" +@:"$pr_head_refname"