On Fri, 28 Jan 2022 at 08:44, Robert Haas <robertmh...@gmail.com> wrote: > OK. I'm still surprised, but it is what it is. I've committed this now.
Thanks > FWIW, I would have been fine with you just committing this change. That's good to know, thanks for mentioning it. FWIW, I just held back as I wasn't 100% sure on the etiquette. David
