[php-src] Issue #10154: Accuracy varies depending on float or string in microtime

Issue: https://github.com/php/php-src/issues/10154 Author: soenke-junike The microtime function can return the time as a string or as a float. float: 1671726894.5131 string: 0.51315000 1671726894 The precision in the string variant is correct to six decimal places: 1671726894.51315 The precision in the float variant is wrong. Here only 4 decimal places are output: 1671726894.5131 It can be easily adjusted with: echo microtime(true);echo "\n";echo microtime(false); In my opinion it can't be caused by any float rounding, because the output of echo hrtime(true) / 1000 / 1000 / 1000; results in 9 decimal places (nanoseconds) as expected. Manual page: https://php.net/function.microtime