UNICODEvsSYMBOL parameter now added everywhere

[helm.git] / helm / on-line / html / library / control.html

diff --git a/helm/on-line/html/library/control.html b/helm/on-line/html/library/control.html
index 57c6c3900e83920432cdbc3f97e61146697fdc41..f70dd94cc9397d6e5a51e71b33ad7ecfe9c1e5d3 100644 (file)
--- a/helm/on-line/html/library/control.html
+++ b/helm/on-line/html/library/control.html
@@ -50,6 +50,7 @@
         '&theoryuri=' + getParam('theoryuri') +
         '&processorURL=' + getParam('processorURL') +
         '&getterURL=' + getParam('getterURL') +
+        '&UNICODEvsSYMBOL=' + getParam('UNICODEvsSYMBOL') +
         '" onClick="refreshReload()">Reload</a>');
      </script>
      <br>
@@ -57,6 +58,7 @@
      <script>
        top.processorURL = getParam('processorURL');
        top.getterURL = getParam('getterURL');
+       top.UNICODEvsSYMBOL = getParam('UNICODEvsSYMBOL');
        top.topurl = getParam('topurl');
        top.mode = getParam('mode');
        top.cicuri = getParam('cicuri');
@@ -90,6 +92,7 @@
         '&theoryuri=' + getParam('theoryuri') +
         '&processorURL=' + getParam('processorURL') +
         '&getterURL=' + getParam('getterURL') +
+        '&UNICODEvsSYMBOL=' + getParam('UNICODEvsSYMBOL') +
         '" onClick="refreshReload()">Configuration Panel</a>');
      </script>
      <br>