As the regular support lifecycle for PHP-7.1 ends on Dec 3rd, 2018 the RM team have decided to make 7.1.25 the last regular 7.1 release (it'll actually come out on the 6th, but horseshoes and handgrenades, right?). As such, since the PHP-7.1.25 release branch has been cut, the PHP-7.1 branch is now locked from casual push, so any diffs which reflect on security should be brought to the attention of the release-managers@ distribution list for inclusion in all security-supported branches.
Thanks to everyone for making PHP happen and Happy Thanksgiving from the American in the room. -Sara
