Closed
Description
Given the well-known reasons for getting rid of the term master
for branches in programming, I would like to push the idea of doing so in this repository.
GitHub default branch renaming is quite sophisticated and I'd expect little interruption for users.
Maintainers would need to make adjustments to CI runners eventually.