Zulip Chat Archive

Stream: new members

Topic: What exactly does `git push` do?

Chris M (Jul 16 2020 at 07:46):

After having read a lot about git, I want to test my understanding:
My understanding is that if one sets up a new repository on github, without adjusting any settings (i.e. this is not talking about mathlib, just my own new unrelated repository), then git push origin does the following: It uploads the commits in my local branch that are not part of the remote origin branch, to the github server. It then checks: if the master branch in the origin repository (i.e. on github) is an ancestor of my local master branch, then it updates the origin/master branch to my local master branch.
i.e. it doesn't do any merging.

However, a github project can set up git push origin to do something other than the default behaviour. In particular, the leanproject has been set up so that it doesn't directly cause the origin/master branch to change, but provides you an option of doing a pull-request via the github website. So rather than git push doing a normal push, it doesn't directly do anything via git, but opens up a github pull-request, which if processed will cause the remote repository to do a pull of my local branch. This mislead me at first.

Is this correct?

Chris Wong (Jul 16 2020 at 07:52):

I don't think GitHub lets you change push behavior in that way

Chris Wong (Jul 16 2020 at 07:53):

Most likely what you're seeing is that the mathlib master branch is locked, and so pushing directly to it will fail

Chris Wong (Jul 16 2020 at 07:53):

After getting that error, a reasonable person would respond by pushing to a differently named branch instead

Chris Wong (Jul 16 2020 at 07:54):

But that's something you do yourself

Last updated: Dec 20 2023 at 11:08 UTC