zulip/tools/reset-to-pull-request

mirror of https://github.com/zulip/zulip.git
#!/bin/sh
set -e
set -x

request_id="$1"
git fetch upstream "pull/$request_id/head"
git reset --hard FETCH_HEAD
Add simple tools for fetching content of a pull request by ID. 2015-12-13 02:06:59 +01:00			`#!/bin/sh`
			`set -e`
			`set -x`

			`request_id="$1"`
tools: Use 'upstream' as expected name for main zulip repo. Fixes: #1698. 2016-08-24 23:23:08 +02:00			`git fetch upstream "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`