We did switch our mainline branch in git to main some while ago. Should we get rid of the old master branch on gitbox and also blow it away on github?
Today I accidentally committed to the master branch, and I'd like to avoid confusion. txs and LieGrue, strub
