php 7.1

Hi folks,

(very) short update here, php 7.1.0 has been released

with two small commits I mentioned in older posts this and that

Nothing big but I have other plans for 7.2 ;-)