On Thu, Apr 30, 2020 at 11:37 AM Peter Geoghegan <[email protected]> wrote: > > The following change fixes it: > > Your fix looks good to me. Please go ahead and commit it.
Actually, never mind. I just pushed your fix myself a moment ago. Thanks again -- Peter Geoghegan
