On Fri, 28 Jan 2022 at 08:44, Robert Haas <robertmhaas@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