DevTools: remove ScriptPreprocessor

Source/devtools/front_end/externs.js

 /*
  * Copyright (C) 2011 Google Inc. All rights reserved.
  *
  * Redistribution and use in source and binary forms, with or without
  * modification, are permitted provided that the following conditions are
  * met:
  *
  *     * Redistributions of source code must retain the above copyright
  * notice, this list of conditions and the following disclaimer.
  *     * Redistributions in binary form must reproduce the above
@@ skipping 272 matching lines @@
     this.startPage = "";
     this.name = "";
 }
 
 /**
  * @constructor
  */
 function ExtensionReloadOptions() {
     this.ignoreCache = false;
     this.injectedScript = "";
-    this.preprocessingScript = "";
     this.userAgent = "";
 }
 
 var Adb = {};
 /** @typedef {{id: string, adbBrowserChromeVersion: string, compatibleVersion: boolean, adbBrowserName: string, source: string, adbBrowserVersion: string}} */
 Adb.Browser;
 /** @typedef {{id: string, adbModel: string, adbSerial: string, browsers: !Array.<!Adb.Browser>, adbPortStatus: !Array.<number>, adbConnected: boolean}} */
 Adb.Device;
 
 /* jsdifflib API */
@@ skipping 416 matching lines @@
  * @return {boolean}
  */
 ArrayBuffer.isView = function(obj) { }
 
 /**
  * @param {Array.<Object>} keyframes
  * @param {number|Object} timing
  * @return {Object}
  */
 Element.prototype.animate = function(keyframes, timing) { }