On Sat, Jun 4, 2016 at 2:56 AM, Robert Haas <robertmhaas@gmail.com> wrote:
> 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.
Thanks you.
--
Michael