Please archive the old github repo since the gerrit report has been created to prevent any confusion about the correct and current code-base.
Extension talk:Sanctions
AchievementBadges, FacetedCategory and Sanctions are now archived on GitHub. Thank you!
Bot name is currently fixed to Korean one, but maybe it can be configurable via MediaWiki messages like on Manual:FixDoubleRedirects.php?
It should Be, but has low priority I think. I created an issue for that. Anyway, Thank you for your kind attention.
There are no older topics