For the record, this got committed as 6bc27698324 in December, along
with the other incremental sort fixes and improvements. I forgot to mark
it as committed in the app, so I've done that now.
regards
--
Tomas Vondra
EnterpriseDB: http://www.enterprisedb.com
The Enterprise PostgreSQL Company