Merge "Follow up 9ef34a2f1d0: fix NewPagesPager "hide registered users" option" into...
authorjenkins-bot <jenkins-bot@gerrit.wikimedia.org>
Fri, 27 Dec 2019 14:53:56 +0000 (14:53 +0000)
committerGerrit Code Review <gerrit@wikimedia.org>
Fri, 27 Dec 2019 14:53:56 +0000 (14:53 +0000)

Trivial merge