Re: [BUG] Possible bug in `remote set-url --add --push`

Andreas Schwab [off-list ref] writes:

Junio C Hamano [off-list ref] writes:

quoted

I actually think my earlier "it shouldn't be the same (push)" is not
needed and probably is actively wrong.  Just like you can tell
between

    (only one .url)                     (both .url and .pushurl)

    origin there (fetch/push)           origin there (fetch)
                                        origin there (push)

What should happen when you have a .pushinsteadof configured that
modifies .url for pushing?

I think push should work like this:

 * the user gives us a nickname;

 * we look at remote.$nickname.pushurl (and if there isn't,
   remote.$nickname.url) to decide the logical URLs to push to;

 * for each logical URL we decided to push, we look at
   url.*.pushInsteadOf to see if there is one that match the $URL
   (and if there isn't url.*.insteadOf), and map the logical URL to
   the final destination.

So that we can instruct "push" to push, when pushing into a
repository that logically resides at git://git.k.org/pub/,
to instead push into the repository via git-over-ssh, e.g.

    [remote "korg"]
	url = git://git.k.org/pub/scm/git/git.git/

    [url "git.k.org:/pub/"]
        pushInsteadOf = git://git.k.org/pub/

without affecting the fetching side.

As I said in a separate message, the above "fetch/push" vs "fetch"
and "push" distinction is not descriptive enough to express the post
rewriting that is done with insteadOf; it only helps debugging
misconfiguration between .url vs .pushurl, which may be better than
the status quo but is not ideal.