On Mon, Dec 08, 2025 at 07:23:16PM +0100, Álvaro Herrera wrote:
> I haven't read this thread, but chanced to come across this and wanted
> to note recent commit c05dee191125. I'm not opposed to changing what
> went in there, but let's make them all the same.
Ah, that must've been where I stole from originally. Will switch it back.
--
nathan