#!/bin/bash set -e usage () { cat >&2 <&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_url=https://api.github.com/repos/"${repo_fq}"/pulls/"${pr_id}" pr_details="$(curl -s "$pr_url")" pr_jq () { echo "$pr_details" | jq "$@" } if [ "$(pr_jq -r .message)" = "Not Found" ]; then echo "Invalid PR URL: $pr_url" exit 1 fi if [ "$(pr_jq .maintainer_can_modify)" != "true" ]; then # This happens when the PR has already been merged or closed, or # if the contributor has turned off the (default) setting to allow # maintainers of the target repo to push to their PR branch. # # The latter 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: PR already closed, or contributor has disallowed pushing to 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"