On Thu, Dec 20, 2018 at 2:45 PM Alvaro Herrera <alvhe...@2ndquadrant.com> 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
