diff --git a/lib/codemirror.js b/lib/codemirror.js index 476ab2e6e521f5432757893da7bfbd548a3956b4..7be2fac1dbb1d4bfb55cd1c59191018769386d33 100644 --- a/lib/codemirror.js +++ b/lib/codemirror.js @@ -4419,7 +4419,7 @@ // Revert a change stored in a document's history. function makeChangeFromHistory(doc, type, allowSelectionOnly) { - if (doc.cm && doc.cm.state.suppressEdits) return; + if (doc.cm && doc.cm.state.suppressEdits && !allowSelectionOnly) return; var hist = doc.history, event, selAfter = doc.sel; var source = type == "undo" ? hist.done : hist.undone, dest = type == "undo" ? hist.undone : hist.done;