marijnh/CodeMirror — pull request #2585 by TheHowl (2014-05-25 13:15:58+00:00)
Title: Update php function library with some extensions

Hi, I updated the file of the php library with the functions of some extensions (json, curl, mysqli) that are pretty much used because:

* json and curl are used for websites API

* mysqli is used since [mysql functions are deprecated in PHP 5.5.0](http://www.php.net/mysql_query)