Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
The conversion done in the previous commits came with hundreds of violations of this rule. While this could be addressed by better types, it will take some work and can be deferred. A new issue/PR will be created after this is merged. <#1864 (comment)>
- Loading branch information