Re: Minor annoyance with git push
- From
Johannes Schindelin <johannes.schindelin@gmx.de>
- Date
- Feb 20, 2008, 13:06 UTC
- Message-ID
- <alpine.LSU.1.00.0802201305350.17164@racer.site>
- In-Reply-To
- <7vzltwavf9.fsf@gitster.siamese.dyndns.org>
Hi,
On Wed, 20 Feb 2008, Junio C Hamano wrote:
Show 5 quoted lines
> Putting this "push = HEAD" by default when "git clone" and "git remote > add" creates the [remote "$remote"] section is probably possible, and at > that stage we may even be able to do the "if the other end is shared, > then set this up automagically", as the result of the magic can be > inspected in the resulting config file.
I think this is too magic, both of it. Once people get used to "git push" being implicitly "git push origin HEAD", why should they not expect "git push <somewhere-else>" to push "HEAD" implicitly, too?
Ciao, Dscho