web/ui/ui.js @@ -845,6 +845,7 @@ lineNumbers: true, mode: m, viewportMargin : Infinity, tabSize: 2, extraKeys: { "F9": function(cm) { cm.setOption("fullScreen", !cm.getOption("fullScreen"));