From: Claudio Sacerdoti Coen Date: Wed, 24 Oct 2001 15:58:16 +0000 (+0000) Subject: Stylesheet to add links menus to graphs added. X-Git-Tag: v0_1_3~49 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f903bcf7b8cb0d05e7fd28912b3bc812f3d4c7ff;p=helm.git Stylesheet to add links menus to graphs added. --- diff --git a/helm/uwobo-panel/control.html b/helm/uwobo-panel/control.html index e8bd1e934..475df6164 100644 --- a/helm/uwobo-panel/control.html +++ b/helm/uwobo-panel/control.html @@ -229,6 +229,7 @@ the getter is used by default (you can deselect it, however): +