From 4ac9fa081a7c045f6a9f1cfc529d82423f485b2e Mon Sep 17 00:00:00 2001
From: Pierre Schmitz <pierre@archlinux.de>
Date: Sun, 8 Dec 2013 09:55:49 +0100
Subject: Update to MediaWiki 1.22.0

---
 profileinfo.php | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

(limited to 'profileinfo.php')

diff --git a/profileinfo.php b/profileinfo.php
index 4117d975..8120599e 100644
--- a/profileinfo.php
+++ b/profileinfo.php
@@ -28,11 +28,7 @@
 ini_set( 'zlib.output_compression', 'off' );
 
 $wgEnableProfileInfo = $wgProfileToDatabase = false;
-if ( isset( $_SERVER['MW_COMPILED'] ) ) {
-	require ( 'core/includes/WebStart.php' );
-} else {
-	require ( __DIR__ . '/includes/WebStart.php' );
-}
+require __DIR__ . '/includes/WebStart.php';
 
 header( 'Content-Type: text/html; charset=utf-8' );
 
@@ -390,8 +386,9 @@ if ( isset( $_REQUEST['filter'] ) ) {
 	}
 
 	$s = new profile_point( 'SQL Queries', 0, $sqltotal, 0, 0 );
-	foreach ( $queries as $q )
+	foreach ( $queries as $q ) {
 		$s->add_child( $q );
+	}
 	$points[] = $s;
 
 	usort( $points, 'compare_point' );
-- 
cgit v1.2.3