diff options
| -rw-r--r-- | webkit/glue/devtools/js/devtools.js | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/webkit/glue/devtools/js/devtools.js b/webkit/glue/devtools/js/devtools.js index 3875cdd..c3f8ac7 100644 --- a/webkit/glue/devtools/js/devtools.js +++ b/webkit/glue/devtools/js/devtools.js @@ -222,10 +222,23 @@ WebInspector.loaded = function() { Preferences.ignoreWhitespace = false; oldLoaded.call(this); + + // Hide dock button on Mac OS. + // TODO(pfeldman): remove once Mac OS docking is implemented. if (InspectorController.platform().indexOf('mac') == 0) { document.getElementById('dock-status-bar-item').addStyleClass('hidden'); } + // Mute refresh action. + document.addEventListener("keydown", function(event) { + if (event.keyIdentifier == 'F5') { + event.preventDefault(); + } else if (event.keyIdentifier == 'U+0052' /* 'R' */ && + (event.ctrlKey || event.metaKey)) { + event.preventDefault(); + } + }, true); + DevToolsHost.loaded(); }; |