From 41a3415c79dd8d1937b89b9ffb921f4409430b77 Mon Sep 17 00:00:00 2001
From: tophf <tophf@gmx.com>
Date: Thu, 30 Jul 2015 01:29:42 +0300
Subject: [PATCH] CodeMirror lint addon init speedup

---
 codemirror/addon/lint/lint.js | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/codemirror/addon/lint/lint.js b/codemirror/addon/lint/lint.js
index 8e3fcb0e..5d54fa54 100644
--- a/codemirror/addon/lint/lint.js
+++ b/codemirror/addon/lint/lint.js
@@ -203,7 +203,7 @@
       if (state.options.tooltips != false)
         CodeMirror.on(cm.getWrapperElement(), "mouseover", state.onMouseOver);
 
-      startLinting(cm);
+      state.timeout = setTimeout(function(){startLinting(cm);}, state.options.delay || 500);
     }
   });