On Wed, Jun 1, 2016 at 7:39 PM, Michael Paquier
<michael.paquier@gmail.com> wrote:
>> In short, I'd vote for putting this change in HEAD, but I see no need to
>> back-patch.
>
> OK, fine for me.
Done.
--
Robert Haas
EnterpriseDB: http://www.enterprisedb.com
The Enterprise PostgreSQL Company