MediaWiki:Gadget-Edittools.js: Difference between revisions