Revision 780c859b4cd2b4407324e25346ec18d2ff013cf1

Committed on 01/11/2018 5:43 am by Johannes Schmitt <schmittjoh@gmail.com> [GitHub Diff]

fixes PHP 7.1 compatibility