From the pull request that @tqchen sent up over the weekend:
Dear TVM Community:
In light of recent proposed change of github’s default branch from master to main. It would be great for the community to consider such a change. Given the minimum impact to set it up. We believe is a net positive to the community and also keeps us up to the latest github convention.
This thread seeks formal lazy consensus
Everyone is also more than welcomed to share their thoughts.
TQ