On Sat, Feb 1, 2020 at 7:37 AM Robert Haas <robertmhaas(at)gmail(dot)com> wrote:> Whoops. The patch looks OK to me.
Pushed.