wikimedia/mediawiki-extensions-DiscussionTools
1
0
Fork 0
mirror of https://gerrit.wikimedia.org/r/mediawiki/extensions/DiscussionTools synced 2024-11-12 01:16:19 +00:00
Code Issues Packages Projects Releases Wiki Activity
mediawiki-extensions-Discus.../.phan
History
jenkins-bot 0e8c9b9536 Merge "Update DiscussionTools phan configuration to match new Parsoid DOM alias config"
2022-01-20 23:34:25 +00:00
..
stubs Don't refer directly to PHP dom extension classes; avoid nonstandard behavior 2021-07-30 18:15:40 -04:00
config.php Merge "Update DiscussionTools phan configuration to match new Parsoid DOM alias config" 2022-01-20 23:34:25 +00:00