cc471140ee66e9d809acf2fb4b57592526e778d8
tdreszer
  Fri May 6 17:54:33 2011 -0700
The nav links are appearing too big in the new CSS scheme.
diff --git src/hg/js/hui.js src/hg/js/hui.js
index 5c8cea6..384b458 100644
--- src/hg/js/hui.js
+++ src/hg/js/hui.js
@@ -1022,31 +1022,31 @@
 function navigationLinksSetup()
 { // Navigation links let you jump to places in the document
   // If they exist, then they need to be well placed to fit window dimensions
 
     // Put navigation links in top corner
     var navDown = $("#navDown");
     if(navDown != undefined && navDown.length > 0) {
         navDown = navDown[0];
         var winWidth = ($(window).width() - 30) + "px"; // Room for borders
         $('.windowSize').css({maxWidth: winWidth,width: winWidth});
         var sectTtl = $("#sectTtl");
         if(sectTtl != undefined && sectTtl.length > 0) {
             $(sectTtl).css({clear: 'none'});
             $(sectTtl).prepend($(navDown));
         }
-        $(navDown).css({'float':'right', 'font-weight':'normal'});
+        $(navDown).css({'float':'right', 'font-weight':'normal','font-size':'medium'});
         $(navDown).show();
     }
 
     // Decide if top links are needed
     var navUp = $('span.navUp');
     if(navUp != undefined && navUp.length > 0) {
         $(navUp).each(function(i) {
             var offset = $(this).parent().offset();
             if(offset.top  > ($(window).height()*(2/3))) {
                 $(this).show();
             }
         });
     }
 }