mirror of https://github.com/zulip/zulip.git
tools: Make remote configurable in {reset,push}-to-pull-request.
The appropriate name for the remote pointing at the repo we maintain may be `upstream` for most of our repos... but not when we're downstream of someone else, e.g. for react-native. So, make it easy to configure per-repo.
This commit is contained in:
parent
d466f3fffc
commit
0462e85d02
|
@ -13,13 +13,18 @@ GitHub to see the subsequent push to master as representing a
|
|||
merge of the PR, rather than requiring the PR to be manually
|
||||
(and to the casual observer misleadingly) closed instead.
|
||||
|
||||
REMOTE defaults to the value of the Git config variable
|
||||
\`zulip.zulipRemote\` if set, else to \`upstream\`.
|
||||
|
||||
See also \`reset-to-pull-request\`.
|
||||
EOF
|
||||
exit 1
|
||||
}
|
||||
|
||||
remote_default="$(git config zulip.zulipRemote || echo upstream)"
|
||||
|
||||
pr_id="$1"
|
||||
remote="${2:-upstream}"
|
||||
remote="${2:-"$remote_default"}"
|
||||
|
||||
if [ -z "$pr_id" ]; then
|
||||
usage
|
||||
|
|
|
@ -1,6 +1,5 @@
|
|||
#!/bin/bash
|
||||
set -e
|
||||
set -x
|
||||
|
||||
if ! git diff-index --quiet HEAD; then
|
||||
set +x
|
||||
|
@ -9,7 +8,12 @@ if ! git diff-index --quiet HEAD; then
|
|||
echo "Doing nothing to avoid losing your work."
|
||||
exit 1
|
||||
fi
|
||||
|
||||
remote_default="$(git config zulip.zulipRemote || echo upstream)"
|
||||
|
||||
request_id="$1"
|
||||
remote=${2:-"upstream"}
|
||||
remote=${2:-"$remote_default"}
|
||||
|
||||
set -x
|
||||
git fetch "$remote" "pull/$request_id/head"
|
||||
git reset --hard FETCH_HEAD
|
||||
|
|
Loading…
Reference in New Issue