On 2023-05-07 00.30, David Holland wrote:
Any reason to not just commit that?
I hadn't done a proper build test yet, and wanted to get the bug documented. I've done a successful build test, and so will commit the fix shortly. Later... Greg Oster