mirror of
https://gerrit.wikimedia.org/r/mediawiki/extensions/CodeMirror
synced 2024-11-23 22:03:28 +00:00
e0dc1c0c32
The service 'GadgetsRepo' gets injected as optional service. This change requires a phan dependency on extension Gadgets in project integration/config in file zuul/parameter_functions.py: I5052e0c666b7dc7af6061e57001f9feac666e029 Change-Id: Ib405ad79b3c348bed51a8938a6a8f73bd35267d2
20 lines
347 B
PHP
20 lines
347 B
PHP
<?php
|
|
|
|
$cfg = require __DIR__ . '/../vendor/mediawiki/mediawiki-phan-config/src/config.php';
|
|
|
|
$cfg['directory_list'] = array_merge(
|
|
$cfg['directory_list'],
|
|
[
|
|
'../../extensions/Gadgets',
|
|
]
|
|
);
|
|
|
|
$cfg['exclude_analysis_directory_list'] = array_merge(
|
|
$cfg['exclude_analysis_directory_list'],
|
|
[
|
|
'../../extensions/Gadgets',
|
|
]
|
|
);
|
|
|
|
return $cfg;
|