Merge "Be more db-friendly when purging expired userrights"
authorjenkins-bot <jenkins-bot@gerrit.wikimedia.org>
Thu, 15 Feb 2018 19:47:47 +0000 (19:47 +0000)
committerGerrit Code Review <gerrit@wikimedia.org>
Thu, 15 Feb 2018 19:47:47 +0000 (19:47 +0000)
commitcead2cadad000dd76751a32743309823ee66294b
tree42e815cec15eefbcc856f683c2e26454978a894a
parent1108e8bac041ae015e9249e7479e743e5598f55a
parentedba39ab602bbcff4aa0f30ce3f7e0dc8bcb6fbb
Merge "Be more db-friendly when purging expired userrights"
includes/DefaultSettings.php