add underline to manage tools page

diff --git a/docs/themes/default/styles.css b/docs/themes/default/styles.css
index fdc4e5b..b0e9715 100644 (file)
--- a/docs/themes/default/styles.css
+++ b/docs/themes/default/styles.css
@@ -1489,7 +1489,7 @@ div#topnavlistcontainer {
        background-image: url('images/pencils_up_bottom.jpg');
        background-position: 99% 0%;
        background-repeat: no-repeat;
-       height:1.8em;
+       height:1.7em;
        margin-top: .1em;
        border-bottom:1px solid #cccccc;
 }
@@ -1570,6 +1570,7 @@ li.top-tool a {  font-weight: bold; }
 li.child-tool a { 
        font-size: x-small;
        font-weight: normal; 
+       text-decoration:underline;
 }
  
 ul.child-top-tool {