Fix: refresh linter if the editor.linter changes

2018-08-31 22:31:44 +08:00 · 2018-08-31 22:31:44 +08:00 · cb77774310
commit cb77774310
parent e7750e7ac9
1 changed files with 4 additions and 0 deletions
--- a/edit/linter.js
+++ b/edit/linter.js
@ -56,3 +56,7 @@ var linter = (() => { // eslint-disable-line no-var
      });
  }
 })();
+
+prefs.subscribe(['editor.linter'], () => {
+  linter.refresh();
+});