Set $_SERVER['SERVER_NAME'] to the value set by --server
authorphysikerwelt <wiki@physikerwelt.de>
Mon, 21 Dec 2015 13:29:02 +0000 (14:29 +0100)
committerPhysikerwelt <wiki@physikerwelt.de>
Thu, 2 Nov 2017 21:42:16 +0000 (21:42 +0000)
commit2de3bf45d12d8d279ae13675500b4ffde65bf5fa
tree6d98f172782b850b4bf4d1f132ff6eb2ec838618
parent6f9738d83242f3195599b1f91e687c2da1a09503
Set $_SERVER['SERVER_NAME'] to the value set by --server

For wiki families that use the "Wikimedia Method" to have domain dependant wikis
the server variable 'SERVER_NAME' might be used to get the database name.
c.f. https://www.mediawiki.org/wiki/Manual:Wiki_family#Wikimedia_Method

This change sets $_SERVER['SERVER_NAME']  to the commandline option passed
as --server to enable the correct loading of the LocalSettings.php

Change-Id: I7e5c009c2403f6c93e81422a8376d7deee4d2b5a
maintenance/Maintenance.php