DevTools extensions: forward keyboard shortcuts to DevTools

Source/devtools/front_end/externs.js

Index: Source/devtools/front_end/externs.js
diff --git a/Source/devtools/front_end/externs.js b/Source/devtools/front_end/externs.js
index a19f2060ca1fe853fe89188ac8715def11810e67..cb2055216f96fcf93e61e5ff9636a126f2bd19f8 100644
--- a/Source/devtools/front_end/externs.js
+++ b/Source/devtools/front_end/externs.js
@@ -46,6 +46,14 @@ Event.prototype.isMetaOrCtrlForTest = false;
 Event.prototype.initWebKitWheelEvent = function(vararg) {}
 Event.prototype.stopImmediatePropagation = function() {}
 
+/**
+ * @constructor
+ * @extends {KeyboardEvent}
+ * @param {string} eventType
+ * @param {Object=} properties
+ */
+window.KeyboardEvent = function(eventType, properties) {}
+
 /** @param {Element} element */
 window.getComputedStyle = function(element) {}
 /** @param {*} message */