This PR is a rebased and squashed version of #7910. As this is the form (in pieces or in whole) that we expect it to be merged in, I’m opening a separate pull request for it. I will leave the old one open for discussion and history.
The tree here is identical to the resulting tree there:
0$ git show -s --format="%T" 3cb46c1a4ac94f4a7f25368bc2ba3c784c901b89
18ddfe56cfedba64667c63dd0fef6ee9584889719
2$ git show -s --format="%T" 17389dc466f2acf8bfa64ce0416f3b5281445a5c
38ddfe56cfedba64667c63dd0fef6ee9584889719
Where 3cb46c1a4ac94f4a7f25368bc2ba3c784c901b89 is #7910’s tip commit, and 17389dc466f2acf8bfa64ce0416f3b5281445a5c is this PR’s tip commit.
Please make comments on #7910, so the history can be tracked, and everything stays in one place.