Update CodeMirror to version 5.15.3

2 files changed, 4 insertions, 3 deletions

diff --git a/public/vendor/codemirror/addon/lint/lint.css b/public/vendor/codemirror/addon/lint/lint.css
index 414a9a0e..f097cfe3 100644
--- a/public/vendor/codemirror/addon/lint/lint.css
+++ b/public/vendor/codemirror/addon/lint/lint.css
@@ -4,10 +4,10 @@
 }
 
 .CodeMirror-lint-tooltip {
-  background-color: infobackground;
+  background-color: #ffd;
   border: 1px solid black;
   border-radius: 4px 4px 4px 4px;
-  color: infotext;
+  color: black;
   font-family: monospace;
   font-size: 10pt;
   overflow: hidden;
diff --git a/public/vendor/codemirror/addon/lint/lint.js b/public/vendor/codemirror/addon/lint/lint.js
index 01f322b5..e3a45276 100644
--- a/public/vendor/codemirror/addon/lint/lint.js
+++ b/public/vendor/codemirror/addon/lint/lint.js
@@ -204,7 +204,8 @@
 
     var annotations = [];
     for (var i = 0; i < spans.length; ++i) {
-      annotations.push(spans[i].__annotation);
+      var ann = spans[i].__annotation;
+      if (ann) annotations.push(ann);
     }
     if (annotations.length) popupTooltips(annotations, e);
   }