git-checkout-pr

$ \cat ~/.local/bin/git-checkout-pr
#!/bin/bash -e
if [[ $# -ne 1 ]] || [[ ! "$1" =~ (^[1-9][0-9]*$) ]]; then
echo "Usage: $0 <pull request ID>" 1>&2
exit 1
fi

ORIGIN='origin'
if git remote | grep -qE '^upstream$'; then
ORIGIN='upstream'
fi

PR_ID="$1"
PR_BRANCH="pr-$PR_ID.$(date '+%Y%m%d%H%M%S')"

echo "Checking out the pull request $PR_ID from $ORIGIN .."
git fetch "$ORIGIN" "pull/$PR_ID/head:$PR_BRANCH"
git checkout "$PR_BRANCH"