| Index: ext/background.js |
| =================================================================== |
| --- a/ext/background.js |
| +++ b/ext/background.js |
| @@ -73,25 +73,16 @@ |
| this._keys.splice(index, 1); |
| this._values.splice(index, 1); |
| } |
| } |
| }; |
| window.ext.PageMap = PageMap; |
| - window.ext.showOptions = function(callback) |
| - { |
| - if (!/\/(?:mobile-)?options\.html/.test(top.location.href)) |
| - window.open("options.html", "_blank"); |
| - |
| - if (callback) |
| - callback(); |
| - }; |
| - |
| window.ext.devtools = { |
| onCreated: { |
| addListener(listener) |
| { |
| window.addEventListener("message", (event) => |
| { |
| if (event.data.type == "devtools") |
| listener(new ext.Page(event.source)); |