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