Merge "resourceloader: Move mw.libs and mw.widgets from startup to mediawiki.base"
authorjenkins-bot <jenkins-bot@gerrit.wikimedia.org>
Mon, 5 Aug 2019 22:11:25 +0000 (22:11 +0000)
committerGerrit Code Review <gerrit@wikimedia.org>
Mon, 5 Aug 2019 22:11:25 +0000 (22:11 +0000)
commit2b1abed0c2163cf7252d35a7da28e8eb96c38881
tree01197eb25e439d612993d1c2c2b72d482795e193
parentf998de6530a24e4dc4b5e9cf97cd8a68ef303b7e
parent46cd3ed7a7c72c3788420d335d86e2dd150d9f18
Merge "resourceloader: Move mw.libs and mw.widgets from startup to mediawiki.base"
resources/src/startup/mediawiki.js