defaults.js no longer in use

diff --git a/helm/on-line/javascript/Makefile b/helm/on-line/javascript/Makefile
index 33ab1ed1cd191aa99e8aa498f1683772242d9fcf..874bf8674f88e61e277a3be3b9b8715a65c58783 100644 (file)
--- a/helm/on-line/javascript/Makefile
+++ b/helm/on-line/javascript/Makefile
@@ -1,5 +1,5 @@
 
-TARGETS = defaults.js_xml helmjsmenu.js_xml
+TARGETS = helmjsmenu.js_xml
 
 .SUFFIXES:
 .SUFFIXES: .js .js_xml

diff --git a/helm/on-line/javascript/defaults.js b/helm/on-line/javascript/defaults.js
deleted file mode 100644 (file)
index c8f89a7..0000000
--- a/helm/on-line/javascript/defaults.js
+++ /dev/null
@@ -1,27 +0,0 @@
-
-function getDefaultParam(name)
-{
-  switch (name) {
-  case "processorURL":
-    return "http://mowgli.cs.unibo.it:8081/helm/servlet/uwobo/";
-  case "getterURL":
-    return "http://mowgli.cs.unibo.it:48081/"; 
-  case "uri_set_queueURL":
-    return "http://mowgli.cs.unibo.it:48082/"; 
-  case "draw_graphURL":
-    return "http://mowgli.cs.unibo.it:48083/"; 
-  case "proofcheckerURL":
-    return "http://mowgli.cs.unibo.it:48084/"; 
-  case "UNICODEvsSYMBOL":
-    return "symbol";
-  case "cicuri":
-    return "cic:/";
-  case "theoryuri":
-    return "theory:/";
-  case "mode":
-    return "processed,cic,html,yes,no,normal,no";
-  }
-  
-  return "???";
-}
-