From dc988a413e9e4a7bbfdd9a0df9be86bf87091956 Mon Sep 17 00:00:00 2001 From: eight Date: Sat, 16 Sep 2017 08:44:56 +0800 Subject: [PATCH] Revert: editors --- edit/lint.js | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/edit/lint.js b/edit/lint.js index 9be438f2..aee241ee 100644 --- a/edit/lint.js +++ b/edit/lint.js @@ -152,7 +152,7 @@ function updateLinter({immediately} = {}) { function updateEditors() { CodeMirror.defaults.lint = linterConfig.getForCodeMirror(linter); const guttersOption = prepareGuttersOption(); - $$('#sections .CodeMirror').map(e => e.CodeMirror).forEach(cm => { + editors.forEach(cm => { cm.setOption('lint', CodeMirror.defaults.lint); if (guttersOption) { cm.setOption('guttersOption', guttersOption);