MediaWiki 1.17.0

[autoinstalls/mediawiki.git] / includes / ProfilerSimple.php

diff --git a/includes/ProfilerSimple.php b/includes/ProfilerSimple.php
index 349a7cac1f42929a333b01ef45fe6ff2a463cadf..8aab1ecc32c443bbac152684dc95cdf4708fd795 100644 (file)
--- a/includes/ProfilerSimple.php
+++ b/includes/ProfilerSimple.php
@@ -4,7 +4,9 @@
  * @ingroup Profiler
  */
 
-require_once(dirname(__FILE__).'/Profiler.php');
+if ( !class_exists( 'Profiler' ) ) {
+       require_once(dirname(__FILE__).'/Profiler.php');
+}
 
 /**
  * Simple profiler base class.
@@ -107,8 +109,9 @@ class ProfilerSimple extends Profiler {
 
        function getCpuTime($ru=null) {
                if ( function_exists( 'getrusage' ) ) {
-                       if ( $ru == null )
+                       if ( $ru == null ) {
                                $ru = getrusage();
+                       }
                        return ($ru['ru_utime.tv_sec'] + $ru['ru_stime.tv_sec'] + ($ru['ru_utime.tv_usec'] +
                                $ru['ru_stime.tv_usec']) * 1e-6);
                } else {
@@ -118,8 +121,9 @@ class ProfilerSimple extends Profiler {
 
        /* 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)
+               if ($time==null) {
                        return microtime(true);
+               }
                list($a,$b)=explode(" ",$time);
                return (float)($a+$b);
        }