Remove REQUEST_TIME_FLOAT hack for old PHP

Change-Id: Id11f4f479d5225d92e38b2ae83b25315591b73d6

diff --git a/includes/WebStart.php b/includes/WebStart.php
index 9ee8042..7bc3039 100644 (file)
--- a/includes/WebStart.php
+++ b/includes/WebStart.php
@@ -32,11 +32,6 @@
 # points and when $wgOut gets disabled or overridden.
 header( 'X-Content-Type-Options: nosniff' );
 
-# Approximate $_SERVER['REQUEST_TIME_FLOAT'] for PHP<5.4
-if ( !isset( $_SERVER['REQUEST_TIME_FLOAT'] ) ) {
-       $_SERVER['REQUEST_TIME_FLOAT'] = microtime( true );
-}
-
 /**
  * @var float Request start time as fractional seconds since epoch
  * @deprecated since 1.25; use $_SERVER['REQUEST_TIME_FLOAT'] or