What exactly does `git push` do?

Stream: new members

[Chris M]

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]

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

[Chris Wong]

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

[Chris Wong]

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

[Chris Wong]

But that's something you do yourself