wikimedia/mediawiki-extensions-InputBox
1
0
Fork 0
mirror of https://gerrit.wikimedia.org/r/mediawiki/extensions/InputBox synced 2024-11-23 14:46:44 +00:00
Code Issues Packages Projects Releases Wiki Activity

Use namespaced ExtensionRegistry class

Browse source 
Change-Id: I7fb6041fa50cc764589a2de1004228b8074dfd4a
This commit is contained in:
Umherirrender 2024-10-20 01:21:10 +02:00
parent 56c2dc45d9
commit d296787dfe
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
includes/InputBox.php
View file

@ -8,12 +8,12 @@
namespace MediaWiki\Extension\InputBox;
use ExtensionRegistry;
use MediaWiki\Config\Config;
use MediaWiki\Html\Html;
use MediaWiki\MainConfigNames;
use MediaWiki\Parser\Parser;
use MediaWiki\Parser\Sanitizer;
use MediaWiki\Registration\ExtensionRegistry;
use MediaWiki\SpecialPage\SpecialPage;
/**