push-to-pull-request: Update local tracking ref, if any.

The companion tool `tools/reset-to-pull-request` has a handy feature
to maintain a local ref tracking the PR: e.g., pr/1234 for PR 1234.
If this were a normal remote-tracking branch maintained by `git fetch`,
it'd get updated on `git push`.  Do the same thing here.

This helps keep a view like `gitk --all @` a bit tidier, by causing
merged PRs to stop pointing at side branches of the main history.
This commit is contained in:
Greg Price
2018-09-11 15:48:20 -07:00
parent bcb16da1e7
commit 3b646c5d28

View File

@@ -22,6 +22,7 @@ EOF
}
remote_default="$(git config zulip.zulipRemote || echo upstream)"
pseudo_remote="$(git config zulip.prPseudoRemote || echo)"
pr_id="$1"
remote="${2:-"$remote_default"}"
@@ -89,5 +90,16 @@ 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
exec git push git@github.com:"$pr_head_repo_fq" +@:"$pr_head_refname"
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