From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 9 Oct 2001 16:42:52 +0000 (+0000)
Subject: Whoops. Forgot to open the CIC file in the cic window.
X-Git-Tag: v0_1_3~71
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f9c6a0ac7617908531633243af1091db829d71fe;p=helm.git

Whoops. Forgot to open the CIC file in the cic window.
---

diff --git a/helm/graphs/tools/mk_html.pl b/helm/graphs/tools/mk_html.pl
index e8c0aed17..08ce976eb 100755
--- a/helm/graphs/tools/mk_html.pl
+++ b/helm/graphs/tools/mk_html.pl
@@ -200,7 +200,7 @@ HM_Array$count = [
 ,,,,,,,,,,,,,,,,
 1,true],
 ["Objects this one depends on.",mkDepURL('$uri'),1,0,1],
-["Render this object.",mkCICURL('$uri'),1,0,0],
+["Render this object.","javascript:window.open('" + mkCICURL('$uri') + "','cic')",1,0,0],
 ["Objects depending on this one.",mkMetaURL('$uri'),1,0,1],
 ];
   </script>