Merge "resourceloader: Merge mediawiki.legacy.wikibits into mediawiki.base"
authorjenkins-bot <jenkins-bot@gerrit.wikimedia.org>
Mon, 5 Aug 2019 22:10:01 +0000 (22:10 +0000)
committerGerrit Code Review <gerrit@wikimedia.org>
Mon, 5 Aug 2019 22:10:01 +0000 (22:10 +0000)
commitf998de6530a24e4dc4b5e9cf97cd8a68ef303b7e
treebf7c28b11faf30eb090f6c18abd08e80d99bf69b
parent0a56880d002134755f8a199910789a9394b4d6fa
parented6e38178bf4d34c38af72deec8bf7d980a670dc
Merge "resourceloader: Merge mediawiki.legacy.wikibits into mediawiki.base"
resources/Resources.php