On Thu, Nov 17, 2022 at 9:02 AM Peter Geoghegan <pg(at)bowt(dot)ie> wrote:> Plan is to commit this later on today, barring objections.
Pushed, thanks.
-- Peter Geoghegan