diff options
-rw-r--r-- | git-fetch-pr | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/git-fetch-pr b/git-fetch-pr new file mode 100644 index 0000000..6b3a80c --- /dev/null +++ b/git-fetch-pr @@ -0,0 +1,17 @@ +#!/bin/sh +# Copyright 2019 Google LLC +# SPDX-License-Identifier: Apache-2.0 + +set -e + +if [ $# -ne 1 ]; then + cat >&2 <<EOF +usage: git fetch-pr https://github.com/[repo]/pull/[number] + +EOF + exit 129 +fi + +exec git fetch $( + echo "$1" | + sed -E 's|^https?://(www\.)?github.com/([^/]+)/([^/]+)/pull/([^/]+).*|https://github.com/\2/\3 refs/pull/\4/head|')
\ No newline at end of file |