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