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
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