So, please ignore my previous patch to the header file, and consider this one - which eliminates it completely.
Thanks, applied.
-Neil
---------------------------(end of broadcast)--------------------------- TIP 5: Have you checked our extensive FAQ?
http://www.postgresql.org/docs/faq