Re: [PATCH v3 1/9] user-manual: Use 'remote add' to setup push URLs

Junio C Hamano wrote:

"W. Trevor King" [off-list ref] writes:

quoted

There is no need to use here documents to setup this configuration.
It is easier, less confusing, and more robust to use `git remote add`
directly.

[...]

This looks like a good 'maint' material that can be applied straight
away there in preparation for 1.8.1.4 to me; reviewers watching from
the sideline, please stop me if you see issues.

Agreed --- this looks good.

[...]

As the additional "remote.public-repo.fetch" line hints, this does
more than "lets you do the same push with just [lazily]"; it also
starts pretending to have run a fetch from there immediately after
you pushed and update the remote tracking branches.  I couldn't
decide if it is a good idea to point it out in this point of the
flow as well, or it is too much detail that is not exactly relevant
while teaching "git push".  I tend to think it would be the latter.

I think it's possible to improve the text here to hint that there's
more to learn (maybe a forward-reference to a section about the
remotes/* hierarchy) without getting lost in the details.  But that
problem was already there, and I don't think it should block this
improvement.

Thanks.
Jonathan