Update to MediaWiki 1.20.2

this update includes:
* adjusted Arch Linux skin
* updated FluxBBAuthPlugin
* patch for https://bugzilla.wikimedia.org/show_bug.cgi?id=44024

1 files changed, 9 insertions, 3 deletions

diff --git a/maintenance/renderDump.php b/maintenance/renderDump.php
index 78c5b6f3..24bedfa4 100644
--- a/maintenance/renderDump.php
+++ b/maintenance/renderDump.php
@@ -28,8 +28,14 @@
  * @ingroup Maintenance
  */
 
-require_once( dirname( __FILE__ ) . '/Maintenance.php' );
+require_once( __DIR__ . '/Maintenance.php' );
 
+/**
+ * Maintenance script that takes page text out of an XML dump file
+ * and render basic HTML out to files.
+ *
+ * @ingroup Maintenance
+ */
 class DumpRenderer extends Maintenance {
 
 	private $count = 0;
@@ -46,7 +52,7 @@ class DumpRenderer extends Maintenance {
 	public function execute() {
 		$this->outputDirectory = $this->getOption( 'output-dir' );
 		$this->prefix = $this->getOption( 'prefix', 'wiki' );
-		$this->startTime = wfTime();
+		$this->startTime = microtime( true );
 
 		if ( $this->hasOption( 'parser' ) ) {
 			global $wgParserConf;
@@ -62,7 +68,7 @@ class DumpRenderer extends Maintenance {
 
 		$importer->doImport();
 
-		$delta = wfTime() - $this->startTime;
+		$delta = microtime( true ) - $this->startTime;
 		$this->error( "Rendered {$this->count} pages in " . round($delta, 2) . " seconds " );
 		if ($delta > 0)
 			$this->error( round($this->count / $delta, 2) . " pages/sec" );