Merge pull request #2722 from henrikt-ma/styling/navbar-font

Better selection of font (including line-height) in navbar
modelica · Nov 19, 2020 · f686111 · f686111
2 parents 0ebd078 + 14c7e7d
commit f686111
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/css/MLS-navbar-left.css b/css/MLS-navbar-left.css
@@ -19,7 +19,8 @@ nav > div.ltx_TOC {
   top: 0px;
   margin: 0px;
   padding: 0px;
-  font: 90% sans-serif;
+  font-size: 14px; /* Less than what is inherited from .body, to reduce need for scrolling. */
+  line-height: 1.3; /* Less than what is inherited from .body, to reduce need for scrolling. */
   color: black;
   border-style: solid;
   border-color: #707A85; /* "Bouncing ball trace gray" */