Hi Hackers, The pull request https://github.com/codemirror/CodeMirror/pull/5814 on CodeMirror was merged and is available in current latest version. This can be marked to be available for next release.
-- Thanks and Regards, Aditya Toshniwal Software Engineer | EnterpriseDB India | Pune "Don't Complain about Heat, Plant a TREE"
