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

Merge "Call Maintenance::requireExtension"

Browse source
This commit is contained in:
jenkins-bot 2020-01-15 09:01:23 +00:00 committed by Gerrit Code Review
parent d6874dcbab fdd52762ee
commit 59bfd520f6
1 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
maintenance/manageForeignResources.php
View file

@ -7,6 +7,12 @@ if ( $IP === false ) {
require_once "$IP/maintenance/Maintenance.php";
class ManageForeignResources extends Maintenance {
public function __construct() {
parent::__construct();
$this->requireExtension( 'DiscussionTools' );
}
public function execute() {
$frm = new ForeignResourceManager(
__DIR__ . '/../modules/lib/foreign-resources.yaml',