#!/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 .message)" = '"Not Found"' ]; then echo "Invalid PR URL: $pr_url" exit 1 fi 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"