Total compatibility with Mozilla 9.1 reached with this commit.

diff --git a/helm/on-line/javascript/prelude.js b/helm/on-line/javascript/prelude.js
index 8b44e1471b6256f5ffbc7fcb71deffc36a8a6370..69479641cd5af9ee32d8ae20aa3d678ee60df6d6 100644 (file)
--- a/helm/on-line/javascript/prelude.js
+++ b/helm/on-line/javascript/prelude.js
@@ -98,11 +98,18 @@ function refreshLinks()
   if (theoryuri == "-1") theoryuri = getDefaultParam("theoryuri");
   if (mode == "-1") mode = getDefaultParam("mode");
 
-  document.links[2].search = "?getterURL=" + getGetterURL();
-  
-  document.links[3].search = 
-    "?processorURL=" + getUwoboURL() +
-    "&getterURL=" + getGetterURL();
+  document.links[2].href =
+   document.links[2].protocol + '//' +
+   document.links[2].host +
+   document.links[2].pathname +
+   "?getterURL=" + getGetterURL();
+
+  document.links[3].href = 
+   document.links[3].protocol + '//' +
+   document.links[3].host +
+   document.links[3].pathname +
+   "?processorURL=" + getUwoboURL() +
+   "&getterURL=" + getGetterURL();
 
   var topurl =
    chopSlash(chopSlash(