On Thu, Dec 20, 2018 at 2:45 PM Alvaro Herrera <[email protected]> wrote: > > OK, cool. If you're going to push a fix for the other changes, do you > > want to do this one too, or should I fix it separately? > > Pushed now.
Thanks. -- Robert Haas EnterpriseDB: http://www.enterprisedb.com The Enterprise PostgreSQL Company
