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
Derk-Jan Hartman 9e24c3a551 RL: Simplify userrights check of Gadgets 
Change-Id: I135dcfdba72014803b8ce9710680fb5574f76d04
2018-08-08 13:46:24 +00:00
..
api
content build: Updating mediawiki/mediawiki-codesniffer to 20.0.0 2018-05-26 03:01:39 +00:00
Gadget.php RL: Simplify userrights check of Gadgets 2018-08-08 13:46:24 +00:00
GadgetDefinitionNamespaceRepo.php Add phan configuration 2018-02-26 12:57:40 -08:00
GadgetHooks.php Fix skins option to use currently displayed skin, rather than user preference 2018-08-01 11:06:17 +10:00
GadgetRepo.php
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-codesniffer to 20.0.0 2018-05-26 03:01:39 +00:00
SpecialGadgets.php Use $lang->equals() to compare Language objects 2018-07-30 20:01:18 +02:00
SpecialGadgetUsage.php Change ResultWrapper to IResultWrapper in special page 2018-04-07 10:35:58 +02:00