Remove workaround for PHP bug 66021 (PHP < 5.5.12)
authorFomafix <fomafix@googlemail.com>
Sun, 16 Apr 2017 21:32:02 +0000 (23:32 +0200)
committerMaxSem <maxsem.wiki@gmail.com>
Thu, 31 May 2018 01:14:58 +0000 (01:14 +0000)
commitbb52950fee26ba2895aadeba0bf7d08fa66dfdd8
tree88ca08d123e7563316b265c58cdc24c7111f53f9
parentb6e8e6b83267e1357bb04edb7976f1a11ee10a5b
Remove workaround for PHP bug 66021 (PHP < 5.5.12)

The PHP bug 66021 <https://bugs.php.net/bug.php?id=66021> was fixed by
https://github.com/php/php-src/pull/518 and is included in PHP 5.4.28+
and PHP 5.5.12+.
This workaround is not necessary anymore because the minimum PHP
version for MediaWiki is 7.0.0+.

Change-Id: I801eaffc253fd88e0d3c87cfe97777837bd3902d
includes/json/FormatJson.php