Bump up the font size of the menu - the last one looked to small on

some browsers.

www/menu.php3

@@ -258,7 +258,7 @@ function WRITESIDEBAR() {
 
     echo "<FORM method=get ACTION=\"/cgi-bin/webglimpse/usr/testbed/webglimpse\">\n";
 ?>
-  <table class="menu" width=200 cellpadding="0" cellspacing="0">
+  <table class="menu" width=210 cellpadding="0" cellspacing="0">
     <tr><td class="menuheader"><b>Information</b></td></tr>
 <?php
     if (0 == strcasecmp($THISHOMEBASE, "emulab.net")) {
@@ -321,7 +321,7 @@ function WRITESIDEBAR() {
     echo "</table>\n";
     echo "</form>\n";
 ?>
-<table class="menu" width=200 cellpadding="0" cellspacing="0">
+<table class="menu" width=210 cellpadding="0" cellspacing="0">
     <tr><td class="menuheader">
       <b>Interaction</b>
     </td></tr>

www/style.css

@@ -77,7 +77,7 @@ td.paddedcell2 { padding: 0.5em; }
 	padding-bottom: 0px;
 	margin: 0px; 
 	border: 0px;
-	font-size: 9pt; }
+	font-size: 10pt; }
 
 .topbaropt {
     	background-color: #fff;