mirror of https://github.com/zulip/zulip.git
push-to-pull-request: Use `git remote get-url`.
This gives us the right behavior when using the `url.*.insteadOf` mechanism for aliases in Git remote URLs. For example, if one's ~/.gitconfig has: [url "git@github.com:"] insteadOf = gh: then `git remote add upstream gh:zulip/zulip` will work great, as the nice, short, mnemonic `gh:` prefix gets expanded to the more finicky `git@github.com:`. I use just such a prefix routinely. But the feature does require that scripts go through the right abstractions. In particular `git remote get-url`, since Git 2.7 (from 2016), exists for exactly this reason. A plain `git config` command bypasses the expansion, getting the verbatim `gh:...` version, which doesn't work. So, switch to that. As a bonus, we get to behave correctly if for some reason the user has configured a push URL distinct from the fetch URL for this remote, just by adding `--push`. With `git config`, we'd have had to manually implement the fallback from `remote.upstream.pushUrl` to `remote.upstream.url` in order to properly handle that case.
This commit is contained in:
parent
6e14c39468
commit
e7a82e732e
|
@ -43,7 +43,7 @@ EOF
|
|||
exit 1
|
||||
fi
|
||||
|
||||
remote_url="$(git config remote."$remote".url)"
|
||||
remote_url="$(git remote get-url --push "$remote")"
|
||||
repo_fq="$(echo "$remote_url" | perl -lne 'print $1 if (
|
||||
m, ^ git\@github\.com:
|
||||
([^/]+ / [^/]+?)
|
||||
|
|
Loading…
Reference in New Issue