Closed bocon13 closed 3 years ago
Agreed to rename the default branch. However, it looks like Github is still working on making the transition seamless for existing repositories: https://github.com/github/renaming/#later-this-year-seamless-move-for-existing-repositories-
We should consider waiting to avoid disruption to other projects depending on this repo (e.g., scripts explicitly referring to master
for git operations)
Yes, I think it makes sense to wait until GitHub sets up branch (git & http) redirection if possible
It looks like Github now has support for branch renaming: https://github.com/github/renaming#rename-existing
It updates existing PRs, supports HTTP redirects, and provides a notice to users of the git CLI.
Also requires renaming 'master' to 'main' on the p4lang repo and updating the default branch in GitHub Settings: https://github.com/github/renaming#rename-existing