]> matita.cs.unibo.it Git - helm.git/commitdiff
Metadata tools are now working correctly also over .body files.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 26 Jun 2003 12:48:03 +0000 (12:48 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 26 Jun 2003 12:48:03 +0000 (12:48 +0000)
helm/on-line/html/cic/control.html

index 02edc199d4644acf75365ea52e94cefb39a47ce1..c6afa7080da0c6ca8b9aa7742b9d79b41b3fb1ff 100644 (file)
@@ -64,6 +64,7 @@ td.back { background-color: #e6e6fa; color: brown }
      url = setParam(url,"xmluri", getterURL + "getxml%3Furi%3D" + CICURI);
      url = setParam(url,"prop.media-type","text/html");
      url = setParam(url,"prop.encoding","iso-8859-1");
+     url = setParam(url,"param.CICURI",CICURI);
      document.write(
       '<a target="metadata" href="' + url + '">View its metadata and dependencies</a>'
      );