Index: Source/devtools/front_end/externs.js |
diff --git a/Source/devtools/front_end/externs.js b/Source/devtools/front_end/externs.js |
index 5efb7ace55027eb5a95f23c9ebb47a914bb142c2..fd5fb6ea760b8bd2230e370cb4724f182cc6809f 100644 |
--- a/Source/devtools/front_end/externs.js |
+++ b/Source/devtools/front_end/externs.js |
@@ -316,6 +316,7 @@ function ExtensionDescriptor() { |
function ExtensionReloadOptions() { |
this.ignoreCache = false; |
this.injectedScript = ""; |
+ this.preprocessingScript = ""; |
this.userAgent = ""; |
} |