On Wed, 26 Oct 2022 at 23:35, David Rowley <dgrowleyml(at)gmail(dot)com> wrote:> I think this is a fairly trivial patch, so if nobody objects, I plan> to push it in the next few days.
Pushed.
David