Re: [WIP/RFC] Allow push and fetch urls to be different

Michael J Gruber [off-list ref] writes:

This introduces a config setting remote.$remotename.pushurl which is
used for pushes only. If absent remote.$remotename.url is used for
pushes and fetches as before.
This is useful, for example, in order to to do passwordless fetches
(remote update) over git: but pushes over ssh.

Signed-off-by: Michael J Gruber <redacted>
---
This is a working prototype, but I'd like to rfc about the approach before
coding further.

As I am guilty for suggesting this, obviously I do not have a problem with
what the patch wants to achieve.

And the change looks simple, straightforward and correct.

Things that would go in a full series:
* documentation (man pages, maybe manual)
* tests

Surely.

* teach builtin-remote about pushurl

Hmm,...  my impression was that "git remote" does not have much support
for the push side.  What kind of things are you going to teach?