From 1daa713582ae156496eb050e3a526dc2dd351268 Mon Sep 17 00:00:00 2001
From: tophf <tophf@gmx.com>
Date: Mon, 4 Sep 2017 01:07:07 +0300
Subject: [PATCH] always hide lint report on switching the linter option

---
 edit/lint.js | 13 ++++---------
 1 file changed, 4 insertions(+), 9 deletions(-)

diff --git a/edit/lint.js b/edit/lint.js
index 09dd6bc4..0fc9d2b3 100644
--- a/edit/lint.js
+++ b/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) {