Thanks. I already have these changes ready in another unmerged branch (9f8f7e97cbdf7ea6d45ba1ec2af8681d9f008a07 and 1796c8e3a7ddc4676b8c66555142432acbc4b498). That branch is not yet ready to be completely merged, but some of the initial commits (including these two) could already go in, so I'm going to merge that instead of this PR.
Thanks. I already have these changes ready in another unmerged branch (9f8f7e97cbdf7ea6d45ba1ec2af8681d9f008a07 and 1796c8e3a7ddc4676b8c66555142432acbc4b498). That branch is not yet ready to be completely merged, but some of the initial commits (including these two) could already go in, so I'm going to merge that instead of this PR.