On Mon, Dec 31, 2018 at 10:50:20AM +0100, Peter Eisentraut wrote:> I like this version of the patch.
OK, committed. Thanks all for the discussion.--Michael