Re: [PATCH v3 2/4] gitfaq: changing the remote of a repository

[Shourya Shukla <shouryashukla.oo@gmail.com>]

On 21/04 12:54, Junio C Hamano wrote:
> Shourya Shukla <shouryashukla.oo@gmail.com> writes:
> 
> > Add issue in 'Common Issues' section which addresses the problem of
> > changing the remote of a repository, covering various cases in which
> > one might want to change the remote and the ways to do the same.
> >
> > Signed-off-by: Shourya Shukla <shouryashukla.oo@gmail.com>
> > ---
> >  Documentation/gitfaq.txt | 31 +++++++++++++++++++++++++++++++
> >  1 file changed, 31 insertions(+)
> 
> Again, I think this belongs to Documentation/git-remote.txt; unlike
> the ".gitignore" one, however, the existing description is heavily
> concentrated on "what happens when X is set to Y?" and does not
> answer "why would I want to set X to Y in the first place?" very
> much.  And the text below you have is a good thing to teach anybody
> who learns "git-remote".  
> 
> So how about clarifying the existing page, perhaps its DISCUSSION
> section (which currently talks only about "how to add a remote, and
> configure" without discussing "why would I want to add a remote, set
> a URL and/or a pushURL to it") with what you have, and trim the
> description here in the FAQ file to the minimum and refer to the
> page instead?

Yep, it seems reasonable. So a good strategy would be to append the
'DISCUSSION' section with what I have added in the FAQ and quoting a
couple of lines from the documentation, providing the solution and
giving a further reference to the Documentation right?

	A remote is an identifier for a location to which Git pushes
	your changes as well as fetches any new changes from (if any).

	To change the remote of your repository, you may want to
	execute:
		git remote set-url <name> <newurl>

Something along the above lines? I think that a generic user will mostly
find this as a solution to their problem instead of using the '--push'
option to specify a different push URL.