- #!/usr/bin/env bash
- set -e
- if [ $# -eq 0 ]; then
- echo "usage: $0 <pull-request-number>"
- exit 1
- fi
- BASE="https://github.com/commaai/openpilot/pull/"
- PR_NUM="$(echo $1 | grep -o -E '[0-9]+')"
- BRANCH=tmp-pr${PR_NUM}
- git branch -D -f $BRANCH || true
- git fetch -u -f origin pull/$PR_NUM/head:$BRANCH
- git switch $BRANCH
- git reset --hard FETCH_HEAD
|