On Thu, May 18, 2017 at 12:13 AM, Robert Haas <robertmhaas(at)gmail(dot)com> wrote:>> Agreed. Committed your patch.>
Thanks Robert!