Rename the master branch to main

[drvinceknight]

I would like to rename the master branch to main.

(There's a tool here that helps with this: https://github.com/mheap/github-default-branch)

[marcharper]

Maybe this is a good time to reconsider the branches "officially". main isn't particularly meaningful from a development standpoint -- is it the main working branch? the current release?

How about a structure such as:

• release in which the HEAD is the most current tagged release
• dev or develop which is the "development stable" (i.e. all tests pass) but not yet released, sort of a staging branch I guess
• people can have other auxiliary branches as needed before merging into dev (e.g. the current ultimatum branch)

When we want to do new releases we just merge dev into release and tag it. New PRs go into dev by default. WDYT?

Next, I'm not sure we need to grant access to a tool for this -- we just push a new branch and tell github that's the new default, right? AFAIK git doesn't have a concept of a default branch (unless that's changed recently), so we just need to set the github default in settings (and delete the old branch).

Also, maybe we want to revisit the contributing instructions and provide a command to setup a venv with the right defaults / dependencies. Seems like we'll need to at least document how people should open PRs and the meaning of the branch names.

[drvinceknight]

How about a structure such as:

• release in which the HEAD is the most current tagged release
• dev or develop which is the "development stable" (i.e. all tests pass) but not yet released, sort of a staging branch I guess
• people can have other auxiliary branches as needed before merging into dev (e.g. the current ultimatum branch)

When we want to do new releases we just merge dev into release and tag it. New PRs go into dev by default. WDYT?

That sounds great and makes the release process more straightforward.

Next, I'm not sure we need to grant access to a tool for this -- we just push a new branch and tell github that's the new default, right? AFAIK git doesn't have a concept of a default branch (unless that's changed recently), so we just need to set the github default in settings (and delete the old branch).

I assumed the tool would take care of any PRs that might be up so that they would automatically "redirect" to the new branch but I'm happy to not use it and just figure out whatever is broken as and when (it won't be anything hard to fix).

Also, maybe we want to revisit the contributing instructions and provide a command to setup a venv with the right defaults / dependencies. Seems like we'll need to at least document how people should open PRs and the meaning of the branch names.

Yeah great call. This could be the first PR to dev 👍

[drvinceknight]

This has been closed by #1372, I have also set the default branch on GitHub to be dev.