diff options
| author | Tim Starling <tstarling@wikimedia.org> | 2020-11-04 10:25:52 +1100 |
|---|---|---|
| committer | Tim Starling <tstarling@wikimedia.org> | 2020-11-04 10:28:22 +1100 |
| commit | 243875ddb9de2d476507944be4c03800d1fcc45c (patch) | |
| tree | ee76d011fd804fb328c710b0e62562f31a7b4f45 /.phan/config.php | |
| parent | f51ccd2ccef8cba0e7d874b6f7cf4b73bcd36636 (diff) | |
| download | mediawikicore-243875ddb9de2d476507944be4c03800d1fcc45c.tar.gz mediawikicore-243875ddb9de2d476507944be4c03800d1fcc45c.zip | |
Local config override file for Phan
Support a local (uncommitted) override file for Phan config. This is
mostly so that I can exclude various broken things, rather than making a
whole new clean source tree just for Phan.
Change-Id: Icc66d8ae2b0029aabf57a57479c54cef05c747b9
Diffstat (limited to '.phan/config.php')
| -rw-r--r-- | .phan/config.php | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/.phan/config.php b/.phan/config.php index ef1eca1a09ce..73fa8d49b025 100644 --- a/.phan/config.php +++ b/.phan/config.php @@ -126,4 +126,9 @@ $cfg['globals_type_map'] = array_merge( $cfg['globals_type_map'], [ 'wgExtraNamespaces' => 'string[]', ] ); +// Include a local config file if it exists +if ( file_exists( __DIR__ . '/local-config.php' ) ) { + require __DIR__ . '/local-config.php'; +} + return $cfg; |