diff --git a/tools/fetch-pull-request b/tools/fetch-pull-request index bd1b425ade..f85640001c 100755 --- a/tools/fetch-pull-request +++ b/tools/fetch-pull-request @@ -1,16 +1,17 @@ #!/usr/bin/env bash set -e -set -x if ! git diff-index --quiet HEAD; then - set +x echo "There are uncommitted changes:" git status --short echo "Doing nothing to avoid losing your work." exit 1 fi + request_id="$1" remote=${2:-"upstream"} + +set -x git fetch "$remote" "pull/$request_id/head" git checkout -B "review-original-${request_id}" git reset --hard FETCH_HEAD diff --git a/tools/fetch-rebase-pull-request b/tools/fetch-rebase-pull-request index 08ddbba6fa..4711f6cb1b 100755 --- a/tools/fetch-rebase-pull-request +++ b/tools/fetch-rebase-pull-request @@ -1,16 +1,17 @@ #!/usr/bin/env bash set -e -set -x if ! git diff-index --quiet HEAD; then - set +x echo "There are uncommitted changes:" git status --short echo "Doing nothing to avoid losing your work." exit 1 fi + request_id="$1" remote=${2:-"upstream"} + +set -x git fetch "$remote" "pull/$request_id/head" git checkout -B "review-${request_id}" "$remote/master" git reset --hard FETCH_HEAD