Update CodeMirror to 5.13.5

2016-04-20 18:11:40 +08:00
parent edc3a31dfd
commit 8bf516263c
84 changed files with 2837 additions and 504 deletions
--- a/public/vendor/codemirror/mode/properties/properties.js
+++ b/public/vendor/codemirror/mode/properties/properties.js
@@ -34,7 +34,7 @@ CodeMirror.defineMode("properties", function() {
      }

      if (sol) {
-        while(stream.eatSpace());
+        while(stream.eatSpace()) {}
      }

      var ch = stream.next();