From ebd6b54e45a9f2fc839fa4da2f57a453553bc433 Mon Sep 17 00:00:00 2001
From: tophf <tophf@gmx.com>
Date: Wed, 17 May 2017 06:15:43 +0300
Subject: [PATCH] Enable linting in newly created styles

---
 edit.js | 1 +
 1 file changed, 1 insertion(+)

diff --git a/edit.js b/edit.js
index 7603c7f6..dbbedf18 100644
--- a/edit.js
+++ b/edit.js
@@ -1133,6 +1133,7 @@ function init() {
 		window.onload = () => {
 			window.onload = null;
 			addSection(null, section);
+			editors[0].setOption('lint', CodeMirror.defaults.lint);
 			// default to enabled
 			document.getElementById("enabled").checked = true
 			initHooks();