origin/main

Stream: general

[Moritz Firsching]

I find it a little bit confusing that there exists a branch main in mathlib,
https://github.com/leanprover-community/mathlib/tree/main
which is not the same as master.
In many other projects that I work on, mainis the current HEAD, so I have accidently checked out main once in a while. In order to prevent that happening to other people, could we perhaps just rename the main branch, for example to laughinggas/main or something. Would that be ok with you, @Ashvni Narayanan ?
If we want to prevent that in the future, probably someone with admin rights can set up a branch protection rule so that is becomes impossible to make a main branch, perhaps also in the mathlib4 repo.

[Reid Barton]

Did you switch main and master in the second half of your message?

[Moritz Firsching]

yes, making my point, I guess..

[Moritz Firsching]

Will edit...

[Gabriel Ebner]

I think you're still mixing up names. We do not have a single branch whose name starts with origin/. We already have a branch protection rule that prevents pushing to master.

[Moritz Firsching]

you are right, I will replace origin/main with main and origin/master with master in what I wrote, then it should be what I mean

[Moritz Firsching]

So my point is to also have a protection rule for main, and having no branch with that name to start with

[Moritz Firsching]

Just in case somebody else also has git checkout origin/main in their muscle memory.

[Moritz Firsching]

fyi, after talking to @Ashvni Narayanan I renamed the main branch to avoid confusion

[Ashvni Narayanan]

Thanks, and sorry for the confusion!

[Moritz Firsching]

Might it be a good idea to delete or rename this branch:
https://github.com/leanprover-community/mathlib4/tree/main to avoid confusion?
@Wrenna Robson

[Moritz Firsching]

Moritz Firsching said:

So my point is to also have a protection rule for main, and having no branch with that name to start with

ceterum censeo

[Wrenna Robson]

Oh yes I don't know how that got in there

[Wrenna Robson]

That's very strange.

[Johan Commelin]

@Wrenna Robson I have deleted the branch. It's contents are now available at the branch wr_main (on the community repo).

[Wrenna Robson]

Thanks. I'm sorry about that - I don't know how it existed to be honest, its contents didn't make much sense to me.