Re: Bug? url.insteadOf overwrites remote.pushUrl

From: Michael J Gruber <git@drmicha.warpmail.net>
Date: Oct 14, 2011, 15:35 UTC
Message-ID: <4E9856BD.3010807@drmicha.warpmail.net>
In-Reply-To: <CAB6D58F-A3C9-4532-A9CC-10E43CD34E4E@jetbrains.com>

Kirill Likhodedov venit, vidit, dixit 14.10.2011 15:55:

> 
> I've found that defining url.<base>.insteadOf overrides explicit
> remote.<name>.pushUrl.

It doesn't really override it. It is applied to it, i.e. transforms it.

> On the other hand, pushInsteadOf doesn't
> override explicit pushUrl. Is it a bug?

That is as described in the thread (thanks for linking to it).

Show 6 quoted lines

> # cat .git/config [remote "origin"] fetch =
> +refs/heads/*:refs/remotes/origin/* url = github.com/klikh/Test.git 
> pushUrl = jetbrains.com/klikh/Test.git [url "http://"] insteadOf=jet
> 
> # git remote -v origin	github.com/klikh/Test.git (fetch) origin
> http://brains.com/klikh/Test.git (push)

The idea of "pushInsteadOf" was that, instead of having to define url and pushurl separately, you can use different rules, say

github -> git://github.com (fetch) github -> https://username@github.com (push) github/ -> git@github.com: (push)

used with "url = github/otheruser/repo.git" alone, without pushurl.

pushurl predates pushinsteadof, and when the latter was introduced, one could have argued for or against "insteadof" being applied to pushurls. But that was necessary before, and existing behavior at the time when pushinsteadof was introduced. So, I don't see a bug, nor anything we could change now, though arguably most people use either pushinstead of or pushurl, but not both.

Cheers, Michael