On Tue, 30 Jan 2024 at 12:25, David Rowley <dgrowleyml(at)gmail(dot)com> wrote:> I'll push this change to master only as there don't seem to have been> any complaints. We can reconsider that if someone complains.
Pushed.
David