On 16.03.23 14:52, Peter Eisentraut wrote:
> On 09.03.23 20:14, Jeff Davis wrote:
>>> Let's come back to that after dealing with the other two.
>>
>> Leaving 0001 open for now.
>
> I suspect making a change like this now would result in a bloodbath on
> the build farm that we could do without. I suggest revisiting this
> after the commit fest ends.
I don't object to this patch. I suggest waiting until next week to
commit it and then see what happens. It's easy to revert if it goes
terribly.
