On Mon, Oct 23, 2023 at 08:44:01PM -0400, Tom Lane wrote:> OK by me.
Cool, done down to 16 as this depends on c8e4030d1bdd.--Michael