diff --git a/tools/push-to-pull-request b/tools/push-to-pull-request index b034822421..b5e16ae9ac 100755 --- a/tools/push-to-pull-request +++ b/tools/push-to-pull-request @@ -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 diff --git a/tools/reset-to-pull-request b/tools/reset-to-pull-request index 405a9927be..a6a4e7bbd0 100755 --- a/tools/reset-to-pull-request +++ b/tools/reset-to-pull-request @@ -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