2016-10-11 20:36:54 +02:00
|
|
|
#!/bin/bash
|
2015-12-13 02:06:59 +01:00
|
|
|
set -e
|
|
|
|
|
set -x
|
|
|
|
|
|
2017-04-12 04:07:17 +02:00
|
|
|
if ! git diff-index --quiet HEAD; then
|
|
|
|
|
set +x
|
2017-05-08 19:51:59 +02:00
|
|
|
echo "There are uncommitted changes:"
|
|
|
|
|
git status --short
|
|
|
|
|
echo "Doing nothing to avoid losing your work."
|
2017-04-12 04:07:17 +02:00
|
|
|
exit 1
|
|
|
|
|
fi
|
2015-12-13 02:06:59 +01:00
|
|
|
request_id="$1"
|
2016-10-11 20:36:54 +02:00
|
|
|
remote=${2:-"upstream"}
|
|
|
|
|
git fetch "$remote" "pull/$request_id/head"
|
2015-12-13 02:06:59 +01:00
|
|
|
git reset --hard FETCH_HEAD
|
