AW: August hiatus and pull requests

> If the group is content to give the group members still reading email over the next month or so editorial discretion, I’m happy to help manage merging editorial PRs during the hiatus.

I’ll be glad to review/approve PRs in August, and I’d be content to see editorial and minor PRs merged before September to avoid conflicts.

Received on Thursday, 20 July 2023 06:08:30 UTC