#!/usr/bin/env bash set -e usage () { cat >&2 </dev/null 2>&1; then 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 "error: invalid PR URL: $pr_url" >&2 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)" tracking_ref= if [ -n "$pseudo_remote" ]; then tracking_ref=$(git rev-parse -q --verify --symbolic refs/remotes/"$pseudo_remote"/"$pr_id" || echo) fi set -x git push git@github.com:"$pr_head_repo_fq" +@:"$pr_head_refname" { set +x; } 2>&- if [ -n "$tracking_ref" ]; then set -x git update-ref "$tracking_ref" @ fi