]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/on-line/javascript/defaults.js
UNICODEvsSYMBOL parameter now added everywhere
[helm.git] / helm / on-line / javascript / defaults.js
index 54d51002ff60b7cfccdb7f27e5eff0fb96270dd9..271f6eabcb8e228401685a4a73746e9a82ba9ffe 100644 (file)
@@ -12,6 +12,8 @@ function getDefaultParam(name)
     return "theory:/";
   case "mode":
     return "processed,cic,html,yes,no,normal,no";
+  case "UNICODEvsSYMBOL":
+    return "symbol";
   }
   
   return "???";