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