Editorial and infrastructure PRs

Hello folks,

I propose that PRs #248, #251, and #253 are either editorial or just
infrastructure tweaking. I’ve approved #248 for Mike, Christian has
approved #251 for me, and #253 clearly just fixes some rendering issues.

If there are no objections, I’ll go ahead and merge those when it’s
convenient. I don’t propose that we need to discuss them on the call
next week.

                                        Be seeing you,
                                          norm

--
Norm Tovey-Walsh
Saxonica

Received on Thursday, 17 November 2022 16:21:39 UTC