On Thu, 20 Oct 2022 at 19:33, David Rowley <dgrowleyml(at)gmail(dot)com> wrote:> I'll push this soon if nobody has any other wording suggestions.
Pushed.
Thanks for the report.
David