#!/bin/bash set -e 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 remote_default="$(git config zulip.zulipRemote || echo upstream)" request_id="$1" remote=${2:-"$remote_default"} set -x git fetch "$remote" "pull/$request_id/head" git reset --hard FETCH_HEAD