diff --git a/tools/fetch-rebase-pull-request b/tools/fetch-rebase-pull-request new file mode 100755 index 0000000000..25dd48d619 --- /dev/null +++ b/tools/fetch-rebase-pull-request @@ -0,0 +1,10 @@ +#!/bin/sh +set -e +set -x + +request_id="$1" +git fetch origin "pull/$request_id/head" +git checkout origin/master -b "review-${request_id}" +git reset --hard FETCH_HEAD +git pull --rebase + diff --git a/tools/reset-to-pull-request b/tools/reset-to-pull-request new file mode 100755 index 0000000000..fcf5d9750b --- /dev/null +++ b/tools/reset-to-pull-request @@ -0,0 +1,7 @@ +#!/bin/sh +set -e +set -x + +request_id="$1" +git fetch origin "pull/$request_id/head" +git reset --hard FETCH_HEAD