Issue 4580 - Replace ext.devtools with devtools

desktop-options.js

 /*
  * 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
@@ skipping 1195 matching lines @@
         updateSubscription(subscription);
         break;
       case "downloading":
       case "downloadStatus":
       case "homepage":
       case "lastDownload":
       case "title":
         updateSubscription(subscription);
         break;
       case "added":
-        let {url, recommended} = subscription;

[Manish Jethani, 2017/10/11 23:48:33]

Unrelated, but this was unused.

+        let {url} = subscription;
         // Handle custom subscription
         if (/^~user/.test(url))
         {
           loadCustomFilters(subscription.filters);
           return;
         }
         else if (url in subscriptionsMap)
           updateSubscription(subscription);
         else
           addSubscription(subscription);
@@ skipping 153 matching lines @@
   });
   chrome.runtime.sendMessage({
     type: "subscriptions.listen",
     filter: ["added", "disabled", "homepage", "lastDownload", "removed",
              "title", "downloadStatus", "downloading"]
   });
 
   window.addEventListener("DOMContentLoaded", onDOMLoaded, false);
   window.addEventListener("hashchange", onHashChange, false);
 }