Huge hack: Opera doesn`t fire an unload event, make sure we can deal with that

options.js

Index: options.js
===================================================================
--- a/options.js
+++ b/options.js
@@ -1,8 +1,24 @@
+// Opera hack: wrap onFilterChange to make sure it won't get called after page
+// unload (Opera doesn't fire the unload event).
+var origOnFilterChange = window.onFilterChange;
+window.onFilterChange = function()
+{
+  if (typeof document.createElement("dummy") === "undefined")
+  {
+    var event = document.createEvent("Events");
+    event.initEvent("unload", false, false);
+    window.dispatchEvent(event);
+    return undefined;
+  }
+  else
+    return origOnFilterChange.apply(this, arguments);
+}
+
 var backgroundPage = opera.extension.bgProcess;
 var require = backgroundPage.require;
 
 with(require("filterClasses"))
 {
   this.Filter = Filter;
   this.WhitelistFilter = WhitelistFilter;
 }