2018-12-18 02:08:53 +01:00
|
|
|
#!/usr/bin/env bash
|
2015-12-13 02:06:59 +01:00
|
|
|
set -e
|
|
|
|
|
2020-10-15 04:55:57 +02:00
|
|
|
usage() {
|
2020-02-11 23:37:42 +01:00
|
|
|
cat >&2 <<EOF
|
|
|
|
usage: $0 PULL_REQUEST_ID [REMOTE]
|
|
|
|
|
|
|
|
Fetch the given GitHub pull request branch, and reset our
|
|
|
|
current branch to it.
|
|
|
|
|
|
|
|
Useful for anyone reading or reviewing a PR, in order to
|
|
|
|
run the code and to study it with a full local set of tools.
|
|
|
|
|
|
|
|
REMOTE defaults to the value of the Git config variable
|
|
|
|
\`zulip.zulipRemote\` if set, else to \`upstream\`.
|
|
|
|
|
|
|
|
If the Git config variable \`zulip.prPseudoRemote\` is set,
|
|
|
|
e.g. with:
|
|
|
|
git config zulip.prPseudoRemote pr
|
|
|
|
then the PR branch is also recorded as a local ref, like a
|
|
|
|
remote-tracking branch as if the PRs make up a "remote". In
|
|
|
|
the example, PR #1234 is recorded as \`pr/1234\`, or in full
|
|
|
|
\`refs/remotes/pr/1234\`. This is useful for keeping track of
|
|
|
|
the PR branch while comparing with other code, and for using
|
|
|
|
the reflog to compare with previous versions of the same PR.
|
|
|
|
|
|
|
|
See also \`push-to-pull-request\`.
|
|
|
|
EOF
|
2017-04-12 04:07:17 +02:00
|
|
|
exit 1
|
2020-02-11 23:37:42 +01:00
|
|
|
}
|
2018-06-22 02:25:49 +02:00
|
|
|
|
|
|
|
remote_default="$(git config zulip.zulipRemote || echo upstream)"
|
2018-07-28 07:25:57 +02:00
|
|
|
pseudo_remote="$(git config zulip.prPseudoRemote || echo)"
|
2018-06-22 02:25:49 +02:00
|
|
|
|
2015-12-13 02:06:59 +01:00
|
|
|
request_id="$1"
|
2018-06-22 02:25:49 +02:00
|
|
|
remote=${2:-"$remote_default"}
|
|
|
|
|
2020-02-11 23:37:42 +01:00
|
|
|
if [ -z "$request_id" ]; then
|
|
|
|
usage
|
|
|
|
fi
|
|
|
|
|
2021-04-30 23:49:33 +02:00
|
|
|
this_dir=${BASH_SOURCE[0]%/*}
|
2020-03-26 02:27:15 +01:00
|
|
|
# shellcheck source=lib/git-tools.bash
|
2021-04-30 23:49:33 +02:00
|
|
|
. "${this_dir}"/lib/git-tools.bash
|
2020-03-26 02:27:15 +01:00
|
|
|
|
|
|
|
require_clean_work_tree 'reset to PR'
|
2020-02-11 23:37:42 +01:00
|
|
|
|
2018-07-28 07:25:57 +02:00
|
|
|
if [ -z "$pseudo_remote" ]; then
|
|
|
|
set -x
|
|
|
|
git fetch "$remote" "pull/$request_id/head"
|
|
|
|
git reset --hard FETCH_HEAD
|
|
|
|
else
|
|
|
|
target_ref=refs/remotes/"$pseudo_remote"/"$request_id"
|
|
|
|
set -x
|
2018-08-03 02:14:50 +02:00
|
|
|
git fetch "$remote" +"pull/$request_id/head:$target_ref"
|
2018-07-28 07:25:57 +02:00
|
|
|
git reset --hard "$target_ref"
|
|
|
|
fi
|