Follow-up to r49646: Untested fix for the problem that bots are now not hidden by...

diff --git a/includes/DefaultSettings.php b/includes/DefaultSettings.php
index 2684ef5..47ae300 100644 (file)
--- a/includes/DefaultSettings.php
+++ b/includes/DefaultSettings.php
@@ -2444,6 +2444,7 @@ $wgDefaultUserOptions = array(
        'rclimit'                 => 50,
        'wllimit'                 => 250,
        'hideminor'               => 0,
+       'rc_hidebots'             => 1,
        'hidepatrolled'           => 0,
        'newpageshidepatrolled'   => 0,
        'highlightbroken'         => 1,