zulip/tools/reset-to-pull-request

#!/bin/bash
set -e
set -x

request_id="$1"
remote=${2:-"upstream"}
git fetch "$remote" "pull/$request_id/head"
git reset --hard FETCH_HEAD
tools: Improve git scripts. Minor fixes that enable the ability to: - Re-run fetch-rebase-pull-request. - Specify the name of the remote repo as an optional second parameter. The default remains 'upstream'. 2016-10-11 20:36:54 +02:00			`#!/bin/bash`
Add simple tools for fetching content of a pull request by ID. 2015-12-13 02:06:59 +01:00			`set -e`
			`set -x`

			`request_id="$1"`
tools: Improve git scripts. Minor fixes that enable the ability to: - Re-run fetch-rebase-pull-request. - Specify the name of the remote repo as an optional second parameter. The default remains 'upstream'. 2016-10-11 20:36:54 +02:00			`remote=${2:-"upstream"}`
			`git fetch "$remote" "pull/$request_id/head"`
Add simple tools for fetching content of a pull request by ID. 2015-12-13 02:06:59 +01:00			`git reset --hard FETCH_HEAD`