--conf option for specifying a different LocalSettings.php. This allows multiple...

diff --git a/maintenance/commandLine.inc b/maintenance/commandLine.inc
index 1fecc0a..c213a2e 100644 (file)
--- a/maintenance/commandLine.inc
+++ b/maintenance/commandLine.inc
@@ -23,6 +23,7 @@ define('MEDIAWIKI',true);
 if ( !isset( $optionsWithArgs ) ) {
        $optionsWithArgs = array();
 }
+$optionsWithArgs[] = 'conf'; # For specifying the location of LocalSettings.php
 
 $self = array_shift( $argv );
 $self = __FILE__;
@@ -141,7 +142,11 @@ if ( file_exists( '/home/wikipedia/common/langlist' ) ) {
        }
 } else {
        $wgWikiFarm = false;
-       $settingsFile = $IP.'/LocalSettings.php';
+       if ( isset( $options['conf'] ) ) {
+               $settingsFile = $options['conf'];
+       } else {
+               $settingsFile = "$IP/LocalSettings.php";
+       }
 
        if ( ! is_readable( $settingsFile ) ) {
                print "A copy of your installation's LocalSettings.php\n" .