wikimedia/mediawiki — pull request #32 by dionysiakontotasiou (2014-10-23 18:57:32+00:00)
Title: Update DefaultSettings.php

Update 67167 mediawiki bug for editmyoptions documentation