MediaWiki:Gadget-CodeEditor.js

/* Broken and not migrated in time (see history) */
mw.log.warn('The CodeEditor gadget has been converted into an extension, and is no longer necessary.');