mediawiki-extensions-Linter/modules/ext.linter.edit.js
James D. Forrester da89d77278 build: Upgrade eslint-config-wikimedia from 0.10.1 to 0.11.0
Change-Id: I17a163c3dd6d708b05d41786dce3dc9881250969
2019-04-03 16:06:08 -07:00

18 lines
545 B
JavaScript

$( function () {
var location = mw.config.get( 'wgLinterErrorLocation' ),
// eslint-disable-next-line no-jquery/no-global-selector
$textbox = $( '#wpTextbox1' );
if ( location ) {
if ( $textbox.length ) {
$textbox.trigger( 'focus' ).textSelection( 'setSelection', { start: location[ 0 ], end: location[ 1 ] } );
}
mw.hook( 've.tempWikitextReady' ).add( function () {
mw.libs.ve.tempWikitextEditor.$element[ 0 ].setSelectionRange(
location[ 0 ], location[ 1 ]
);
mw.libs.ve.tempWikitextEditor.focus();
} );
}
} );