Zulip Chat Archive

Stream: new members

Topic: What exactly does `git push` do?


view this post on Zulip 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?

view this post on Zulip Chris Wong (Jul 16 2020 at 07:52):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Chris Wong (Jul 16 2020 at 07:54):

But that's something you do yourself


Last updated: May 11 2021 at 13:22 UTC