--On 5. April 2016 21:50:17 -0400 Robert Haas <robertmhaas(at)gmail(dot)com> wrote:
> If nobody's going to commit this right away, this should be added to> the next CommitFest so we don't forget it.
Done.
-- Thanks
Bernd