> On 13 May 2024, at 10:48, Peter Eisentraut <peter(at)eisentraut(dot)org> wrote:
> Patches attached.
All patches look good.
> I think the first one is a bug fix.
Agreed.
--Daniel Gustafsson