Chromium Code Reviews
chromiumcodereview-hr@appspot.gserviceaccount.com (chromiumcodereview-hr) | Please choose your nickname with Settings | Help | Chromium Project | Gerrit Changes | Sign out
(267)

Unified Diff: third_party/WebKit/Source/devtools/front_end/externs.js

Issue 2498783002: DevTools: [Sources] Improve editor load time by optimizing setMimeType (Closed)
Patch Set: installMimeTypeModes Created 4 years, 1 month ago
Use n/p to move between diff chunks; N/P to move between comments. Draft comments are only viewable by you.
Jump to:
View side-by-side diff with in-line comments
Download patch
Index: third_party/WebKit/Source/devtools/front_end/externs.js
diff --git a/third_party/WebKit/Source/devtools/front_end/externs.js b/third_party/WebKit/Source/devtools/front_end/externs.js
index fb308e40c34931de1160799995826ab03b0aba26..ce5dd2e324a988bb66deaa3d99f8dc20024f02f3 100644
--- a/third_party/WebKit/Source/devtools/front_end/externs.js
+++ b/third_party/WebKit/Source/devtools/front_end/externs.js
@@ -529,6 +529,8 @@ CodeMirror.prototype = {
};
/** @type {!{cursorDiv: Element}} */
CodeMirror.prototype.display;
+/** @type {!{mode: string}} */
+CodeMirror.prototype.options;
/** @type {!Object} */
CodeMirror.Pass;
CodeMirror.showHint = function(codeMirror, hintintFunction) {};

Powered by Google App Engine
This is Rietveld 408576698