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 "$@"