New HELM interface almost stable.

[helm.git] / helm / on-line / javascript / control.js

diff --git a/helm/on-line/javascript/control.js b/helm/on-line/javascript/control.js
index bc52d02b617d6a2948d56b65dcaf4d103528d862..0e6e566a05d46f4049a9ebeeef6265c713f813ce 100644 (file)
--- a/helm/on-line/javascript/control.js
+++ b/helm/on-line/javascript/control.js
@@ -258,3 +258,4 @@ function makeURL(type,uri,cicflags,typesflags,profile,processorURL,interfaceURL,
   else if (type == "theory")
    return processorURL + "apply?keys=RT&xmluri=" + escape(thinterfaceURLidx) + "&param.ignore=" + keys + "&param.CICURI=" + uri;
 }
+