On Thu, Oct 12, 2023 at 1:09 AM Tom Lane <[email protected]> wrote:

> Pushed after a bit of fiddling with the comment.


Thanks for pushing!

Thanks
Richard

Reply via email to