On Sat, May 11, 2019 at 11:02 AM Bruce Momjian <bruce(at)momjian(dot)us> wrote:> OK, commit removed.
You're mistaken -- nothing has been pushed to master in the last 3 hours.
-- Peter Geoghegan