From 7c5b4c2bcfe8bad8cc5bf5bd5c49915016faf0fc Mon Sep 17 00:00:00 2001 From: Rob Garrison Date: Sun, 20 Aug 2017 09:10:44 -0500 Subject: [PATCH] Remove extra delay It appears to no longer be an issue --- edit/edit.js | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/edit/edit.js b/edit/edit.js index 35f4b9d1..1f997dba 100644 --- a/edit/edit.js +++ b/edit/edit.js @@ -1227,8 +1227,7 @@ function initWithStyle({style, codeIsUpdated}) { if (CodeMirror.lint) { setTimeout(() => { cm.setOption('lint', CodeMirror.defaults.lint); - // update lint issue table after a short delay - updateLintReport(cm, 200); + updateLintReport(cm, 0); }, prefs.get('editor.lintDelay')); } }