[MediaWiki-commits] [Gerrit] Allow other extensions to add or override discovery tools - change (mediawiki...MobileFrontend)

jenkins-bot has submitted this change and it was merged. Change subject: Allow other extensions to add or override discovery tools .. Allow other extensions to add or override discovery tools Change-Id:

[MediaWiki-commits] [Gerrit] Allow other extensions to add or override discovery tools - change (mediawiki...MobileFrontend)

Bmansurov has uploaded a new change for review. https://gerrit.wikimedia.org/r/191219 Change subject: Allow other extensions to add or override discovery tools .. Allow other extensions to add or override discovery tools