marijnh/CodeMirror — pull request #1371 by adhintz (2013-03-16 07:48:55+00:00)
Title: Remove Opera-specific CSS properties where not needed

-o-border-radius is not a real property.
Opera supports border-radius and box-shadow.