On Thu, Oct 12, 2023 at 1:09 AM Tom Lane <tgl(at)sss(dot)pgh(dot)pa(dot)us> wrote:
> Pushed after a bit of fiddling with the comment.
Thanks for pushing!
ThanksRichard