marijnh/CodeMirror — pull request #855 by peterkroon (2012-09-28 10:45:17+00:00)
Title: [v3] update codemirror.js / lineWidgets

Make sure that the lineWidget is still visible when making a selection in the editor