SERVER['REQUEST_TIME'] vs SERVER['REQUEST_TIME_FLOAT']

[mbischof]

PHP_TIMER requires php version gt 5.3.3
$_SERVER['REQUEST_TIME_FLOAT'] is available since php version 5.4.0

so, if SERVER['REQUEST_TIME_FLOAT'] is not available use SERVER['REQUEST_TIME']

[sebastianbergmann]

You mean like this

diff --git a/PHP/Timer.php b/PHP/Timer.php
index 0056ea8..5f62445 100644
--- a/PHP/Timer.php
+++ b/PHP/Timer.php
@@ -143,6 +143,10 @@ public static function resourceUsage()
     PHP_Timer::$requestTime = $_SERVER['REQUEST_TIME_FLOAT'];
 }

+else if (isset($_SERVER['REQUEST_TIME'])) {
+    PHP_Timer::$requestTime = $_SERVER['REQUEST_TIME'];
+}
+
 else {
     PHP_Timer::$requestTime = microtime(TRUE);
 }