wikimedia/mediawiki-extensions-Gadgets
1
0
Fork 0
mirror of https://gerrit.wikimedia.org/r/mediawiki/extensions/Gadgets synced 2024-11-15 11:31:40 +00:00
Code Issues Packages Projects Releases Wiki Activity
mediawiki-extensions-Gadgets/includes
History
Umherirrender 7c13328467 build: Updating mediawiki/mediawiki-phan-config to 0.8.0 
Argument 1 ($min) is 7000000.0 but \mt_rand() takes int
Argument 2 ($max) is 15000000.0 but \mt_rand() takes int

Bug: T235049
Change-Id: I2d7d0d6defd312dbed0de833678f3768fa3d7a46
2019-11-03 12:13:20 +01:00
..
api Upgrade to newer phan 2019-03-17 16:39:02 -07:00
content build: Updating mediawiki/mediawiki-codesniffer to 20.0.0 2018-05-26 03:01:39 +00:00
Gadget.php Update some generic/unspecific PHPDoc type hints 2019-06-04 17:33:17 +02:00
GadgetDefinitionNamespaceRepo.php Upgrade to newer phan 2019-03-17 16:39:02 -07:00
GadgetHooks.php phan: Remove suppression for PhanParamTooMany 2019-10-04 11:46:21 +02:00
GadgetRepo.php Avoid hardcoding specific GadgetRepo implementations for cache invalidations 2017-11-07 12:13:11 -08:00
GadgetResourceLoaderModule.php build: Updating mediawiki/mediawiki-codesniffer to 20.0.0 2018-05-26 03:01:39 +00:00
MediaWikiGadgetsDefinitionRepo.php build: Updating mediawiki/mediawiki-phan-config to 0.8.0 2019-11-03 12:13:20 +01:00
SpecialGadgets.php Add help links to special pages 2019-07-18 01:35:23 +00:00
SpecialGadgetUsage.php Add help links to special pages 2019-07-18 01:35:23 +00:00