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