Fixes #759: go back to history when closing diff

[redakcja.git] / redakcja / static / js / lib / codemirror / codemirror.js

diff --git a/redakcja/static/js/lib/codemirror/codemirror.js b/redakcja/static/js/lib/codemirror/codemirror.js
index 8c62dab..8475989 100644 (file)
--- a/redakcja/static/js/lib/codemirror/codemirror.js
+++ b/redakcja/static/js/lib/codemirror/codemirror.js
@@ -177,8 +177,8 @@ var CodeMirror = (function(){
     replaceChars: function(text, start, end) {
       this.editor.replaceChars(text, start, end);
     },
-    getSearchCursor: function(string, fromCursor) {
-      return this.editor.getSearchCursor(string, fromCursor);
+    getSearchCursor: function(string, fromCursor, regexp, case_sensitive) {
+      return this.editor.getSearchCursor(string, fromCursor, regexp, case_sensitive);
     },
 
     undo: function() {this.editor.history.undo();},