Apparently this patch now has a duplicate OID. Please do use random
OIDs >8000 as suggested by the unused_oids script.
--
Álvaro Herrera https://www.2ndQuadrant.com/
PostgreSQL Development, 24x7 Support, Remote DBA, Training & Services