diff options
author | Benjamin Barenblat <benjamin@barenblat.name> | 2020-06-01 10:59:33 -0400 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-01 10:59:33 -0400 |
commit | e6129fa5e485cafde161adbaf3925f7ac7a7cde9 (patch) | |
tree | d2ae95a568cd0b6dc10adc91d76209c7d0f9296f |
-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 |