I wrote:> Will push a fix in a few minutes.
And done. Should be possible to revert 7d3bf73ac, if you wish.
regards, tom lane