I'd like to change the name of the `master` branch to `main` following many [others](https://www.theserverside.com/feature/Why-GitHub-renamed-its-master-branch-to-main). Basic instructions are [here](https://git-scm.com/book/en/v2/Git-Branching-Branch-Management). @speleo3 or others -- any concerns? I'll wait a week or so before making the change.