flintlib / python-flint

Python bindings for Flint and Arb
MIT License
131 stars 25 forks source link

Rename `master` to `main` #213

Closed GiacomoPope closed 1 month ago

GiacomoPope commented 1 month ago

This is generally considered best practice now, are there any reasons not to make this change?

oscarbenjamin commented 1 month ago

No, no reason. It creates a bit of awkwardness because people need to update their clones but that's a temporary problem.

oscarbenjamin commented 1 month ago

Okay I've set the default branch to main.

Anyone with an existing clone needs to do:

# Switch to the "master" branch:
$ git checkout master

# Rename it to "main":
$ git branch -m master main

# Get the latest commits (and branches!) from the remote:
$ git fetch

# Remove the existing tracking connection with "origin/master":
$ git branch --unset-upstream

# Create a new tracking connection with the new "origin/main" branch:
$ git branch -u origin/main
oscarbenjamin commented 1 month ago

Oh, and this invalidates all open PRs I think.

oscarbenjamin commented 1 month ago

Oh, and this invalidates all open PRs I think.

No, it doesn't. I managed to change the base branch to main in all of the open PRs. I think that maybe was not possible in the distant past.