mirror of https://github.com/zulip/zulip.git
67 lines
2.0 KiB
Plaintext
67 lines
2.0 KiB
Plaintext
|
#!/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"
|