Revert: editors

This commit is contained in:
eight 2017-09-16 08:44:56 +08:00
parent 4d6f856473
commit dc988a413e

View File

@ -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);