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