WIP Wednesday: 12 Feb 2023

Lots of small pull requests merged in this past week (which is as it should be!). Nothing Earth-shattering, just continued incremental improvement. In the next week:

PR stats: In the week from Tuesday, 7 Jan to Tuesday, 14 Jan there were 54 pull requests merged, with a total codebase change of +3,170 / ‑2,251 lines (not counting translation changes). That’s an average merged PR size of +58/ ‑42.