]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/graphs/tools/mk_html.pl
New implementation: now the number of nodes is used to prune the graph
[helm.git] / helm / graphs / tools / mk_html.pl
index 5c1daa5b87e2592b304af2de5a3071b542195cf3..b98e38de13af906ff681087dc09fc57e983ae6ba 100755 (executable)
@@ -107,7 +107,7 @@ EOT
    var iurl = unescape(getParam("url"));
    var getterURL = getParam3(iurl,"param.getterURL");
    var interfaceURL = unescape(getParam3(iurl,"param.interfaceURL"));
-   var url = setParam(iurl,"keys","d_c%2CC1%2CHC2%2CL");
+   var url = setParam(iurl,"keys",getParam3(iurl,"param.keys"));
    url = setParam(url,"xmluri", getterURL + "getxml%3Furi%3D$uri");
    url = setParam(url,"param.CICURI","$uri");
    url = setParam(url,"param.RDFURI","helm:rdf:www.cs.unibo.it/helm/rdf/rdfprova//$uri");