diff options
Diffstat (limited to '.local/bin/git-fetch-pr')
-rwxr-xr-x | .local/bin/git-fetch-pr | 42 |
1 files changed, 42 insertions, 0 deletions
diff --git a/.local/bin/git-fetch-pr b/.local/bin/git-fetch-pr new file mode 100755 index 0000000..ba9fa2d --- /dev/null +++ b/.local/bin/git-fetch-pr @@ -0,0 +1,42 @@ +#!/bin/bash +set -euE + +is_int() { + local re='^[0-9]+$' + [[ $1 =~ $re ]] +} + +errusage() { + if [[ $# != 0 ]]; then + echo >&2 "${0##*/}: error: $*" + fi + echo >&2 "Usage: ${0##*/} [REMOTE] PR_NUMS..." + return 2 +} + +main() { + if [[ $# == 0 ]]; then + errusage 'require 1 or more PR numbers' + fi + local remote=origin + if ! is_int "$1"; then + remote=$1 + shift + if [[ $# == 0 ]]; then + errusage 'require 1 or more PR numbers' + fi + fi + local refspecs=() + for pr in "$@"; do + if ! is_int "$pr"; then + errusage "not a number: ${pr@Q}" + fi + refspecs+=( + "refs/pull/${pr}/head:refs/pull/${pr}/head" + #"refs/pull/${pr}/merge:refs/pull/${pr}/merge" + ) + done + git fetch --force "$remote" "${refspecs[@]}" +} + +main "$@" |