Update to MediaWiki 1.19.0

1 files changed, 0 insertions, 9 deletions

diff --git a/includes/profiler/ProfilerSimple.php b/includes/profiler/ProfilerSimple.php
index bbdbec8e..055a0ea0 100644
--- a/includes/profiler/ProfilerSimple.php
+++ b/includes/profiler/ProfilerSimple.php
@@ -115,13 +115,4 @@ class ProfilerSimple extends Profiler {
 			return 0;
 		}
 	}
-
-	/* If argument is passed, it assumes that it is dual-format time string, returns proper float time value */
-	function getTime($time=null) {
-		if ($time==null) {
-			return microtime(true);
-		}
-		list($a,$b)=explode(" ",$time);
-		return (float)($a+$b);
-	}
 }