From cb777743107c8d16aa32a3b618a269ef4b2cd296 Mon Sep 17 00:00:00 2001
From: eight <eight04@gmail.com>
Date: Fri, 31 Aug 2018 22:31:44 +0800
Subject: [PATCH] Fix: refresh linter if the editor.linter changes

---
 edit/linter.js | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/edit/linter.js b/edit/linter.js
index 6053b4e7..89e3beb9 100644
--- 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();
+});