installer: Add support for PlatformSettings.php
PlatformSettings.php is a standardized and recommended way for
re-distributors and packagers of MediaWiki to be able to tune
DefaultSettings.php as appropriate.
If includes/PlatformSettings.php exists, the installer will
automatically include it as part of the generated LocalSettings.php.
The main advantage of this system is that if the distributor wants to
change the default settings, all users will benefit immediately. And if
people want a vanilla MediaWiki experience, they can just remove the
inclusion from their LocalSettings.php.
This RfC
(<https://www.mediawiki.org/wiki/Requests_for_comment/PlatformSettings.php>)
was approved by TechCom.
Bug: T182020
Change-Id: I34f9a4acbe86b9c5c80ac16451b317ce5f6640f9