reverting my unintended change in DefaultSettings.php
authorThomas Gries <wikinaut@users.mediawiki.org>
Wed, 10 Aug 2011 05:58:21 +0000 (05:58 +0000)
committerThomas Gries <wikinaut@users.mediawiki.org>
Wed, 10 Aug 2011 05:58:21 +0000 (05:58 +0000)
commitbab1c5b6182b7cfe5c552722c5033d5694a7569e
tree2483fcf8908412c64155bf9e0a570853d8547def
parentc6ec5a6d8d5fc420261f645921c458baea3f61a7
reverting my unintended change in DefaultSettings.php
includes/DefaultSettings.php