Use PHP5 version of function microtime()
The PHP function microtime() delivered a string that has the current unixtime and the microseconds divided by a spacing character. These two parts are currently exploded by that space character and summarized. With PHP5 it's possible to use microtime(true) to get the same.
(issue imported from #M11267)