wikimedia/mediawiki-extensions-DiscussionTools
1
0
Fork 0
mirror of https://gerrit.wikimedia.org/r/mediawiki/extensions/DiscussionTools synced 2024-11-24 08:23:52 +00:00
Code Issues Packages Projects Releases Wiki Activity
mediawiki-extensions-Discus.../maintenance
History
Umherirrender fdd52762ee Call Maintenance::requireExtension 
This avoids that the script is executed without the extension is
installed.
This avoids than an error when class is missing

Change-Id: I064d2be5dbaa3b43c8134e19694511398decba88
2020-01-13 22:15:43 +01:00
..
manageForeignResources.php Call Maintenance::requireExtension 2020-01-13 22:15:43 +01:00