wikimedia/mediawiki-extensions-Gadgets
1
0
Fork 0
mirror of https://gerrit.wikimedia.org/r/mediawiki/extensions/Gadgets synced 2024-11-14 19:14:45 +00:00
Code Issues Packages Projects Releases Wiki Activity

Bump MediaWikiGadgetsDefinitionRepo cache version

Browse source 
Bug: T303455
Change-Id: I32138cd8547f8c5773cbe603fdeb9826e04b0461
This commit is contained in:
Alexander Vorwerk 2022-03-09 20:32:12 +01:00
parent ba83b57d1d
commit 1f40a76cc0
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
includes/MediaWikiGadgetsDefinitionRepo.php
View file

@ -16,7 +16,7 @@ use Wikimedia\Rdbms\Database;
* Gadgets repo powered by MediaWiki:Gadgets-definition
*/
class MediaWikiGadgetsDefinitionRepo extends GadgetRepo {
private const CACHE_VERSION = 2;
private const CACHE_VERSION = 3;
/** @var array|false|null */
private $definitionCache;