Merge "Setup: Deprecate StartProfiler, move default to DefaultSettings"
authorjenkins-bot <jenkins-bot@gerrit.wikimedia.org>
Tue, 17 Apr 2018 20:22:23 +0000 (20:22 +0000)
committerGerrit Code Review <gerrit@wikimedia.org>
Tue, 17 Apr 2018 20:22:23 +0000 (20:22 +0000)
commit8519b66979096124a4a6e1720937a501d720fd5b
tree35a43d7ee0b4cba208947738bba24b590844c94b
parent69257de17fc899c447c9f1229b6ed319bc05d316
parent5209adff6cf13a002843347d5e3942aeb5c255ce
Merge "Setup: Deprecate StartProfiler, move default to DefaultSettings"
includes/DefaultSettings.php