Issue 4580 - Replace ext.devtools with devtools

ext/devtools.js

Index: ext/devtools.js
===================================================================
deleted file mode 100644
--- a/ext/devtools.js
+++ /dev/null
@@ -1,33 +0,0 @@
-/*
- * This file is part of Adblock Plus <https://adblockplus.org/>,
- * Copyright (C) 2006-present eyeo GmbH
- *
- * Adblock Plus is free software: you can redistribute it and/or modify
- * it under the terms of the GNU General Public License version 3 as
- * published by the Free Software Foundation.
- *
- * Adblock Plus is distributed in the hope that it will be useful,
- * but WITHOUT ANY WARRANTY; without even the implied warranty of
- * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
- * GNU General Public License for more details.
- *
- * You should have received a copy of the GNU General Public License
- * along with Adblock Plus.  If not, see <http://www.gnu.org/licenses/>.
- */
-
-"use strict";
-
-if (typeof ext == "undefined")
-  window.ext = {};
-
-window.ext.devtools = {
-  panels: {
-    openResource() {}
-  },
-
-  inspectedWindow: {
-    reload() {}
-  }
-};
-
-window.ext.backgroundPage._sendRawMessage({type: "devtools"});