Code cleanup: more code sharing achieved.

diff --git a/helm/on-line/javascript/graphLinks.js b/helm/on-line/javascript/graphLinks.js
index 9cad277a7eff3d6b5a197c067c238dd11f6247a4..c95c85a45a6151415df35f536756fb1fcb258f94 100644 (file)
--- a/helm/on-line/javascript/graphLinks.js
+++ b/helm/on-line/javascript/graphLinks.js
@@ -75,7 +75,7 @@ function mkMetaTheoryURL(uri)
 {
    var rdfuri = mkRDFURI(uri);
    var getterURL = getParam("param.getterURL");
-   var url = setParam(location.href,"keys","meta_theory,T1,T2,L,E");
+   var url = setParam(location.href,"keys","meta_theory," + unescape(getTheoryKeys()));
    url = setParam(url,"xmluri", getterURL + "getxml%3Furi%3D" + rdfuri);
    return url;
 }