OK, pushed. This soon caused buildfarm to show a failure due to
underspecified ORDER BY, so I just pushed a fix for that too.
Thanks Simon for reporting the problem, and thanks Amit for the patch.
--
Álvaro Herrera Breisgau, Deutschland — https://www.EnterpriseDB.com/
"Si quieres ser creativo, aprende el arte de perder el tiempo"