Ævar Arnfjörð Bjarmason" <avarab@xxxxxxxxx> wrote: > Let's use "git push <remote> HEAD" which always means push the current > branch name to that remote, instead of "git push <remote> > <current-branch-name>" which will do that under "simple", but is not > guaranteed to do under "upstream". Probably a good idea indeed. One potential objection though: I think many people know git push origin master (not that they necessarily understand it, but I've seen many people talking or asking questions about what "origin master" is) This "git push origin HEAD" is IMHO less common. It may confuse users. Or users may learn it and be happy thanks to your message. I don't know. -- Matthieu Moy https://matthieu-moy.fr/
