always hide lint report on switching the linter option
This commit is contained in:
parent
36d790e0c2
commit
1daa713582
13
edit/lint.js
13
edit/lint.js
|
@ -144,6 +144,10 @@ function updateLinter({immediately} = {}) {
|
|||
const linter = prefs.get('editor.linter');
|
||||
const GUTTERS_CLASS = 'CodeMirror-lint-markers';
|
||||
|
||||
loadLinterAssets(linter).then(updateEditors);
|
||||
$('#linter-settings').style.display = !linter ? 'none' : 'inline-block';
|
||||
$('#lint').style.display = 'none';
|
||||
|
||||
function updateEditors() {
|
||||
CodeMirror.defaults.lint = linterConfig.getForCodeMirror(linter);
|
||||
const guttersOption = prepareGuttersOption();
|
||||
|
@ -182,15 +186,6 @@ function updateLinter({immediately} = {}) {
|
|||
el.remove();
|
||||
}
|
||||
}
|
||||
|
||||
// load scripts
|
||||
loadLinterAssets(linter).then(() => {
|
||||
updateEditors();
|
||||
});
|
||||
$('#linter-settings').style.display = !linter ? 'none' : 'inline-block';
|
||||
if (!linter) {
|
||||
$('#lint').style.display = 'none';
|
||||
}
|
||||
}
|
||||
|
||||
function updateLintReport(cm, delay) {
|
||||
|
|
Loading…
Reference in New Issue
Block a user