From 14c7e7dca19ca783b11eb6df8def4cf0e0382a30 Mon Sep 17 00:00:00 2001 From: Henrik Tidefelt Date: Wed, 18 Nov 2020 09:46:03 +0100 Subject: [PATCH] Better selection of font (including line-height) in navbar The previous use of the CSS 'font' property was implying a 'line-height' of 1.0, making the table of contents rather hard to read. By specifying 'font-size' and 'line-height' instead, we can not ensure that the font face is the same sans-serif as set in .body, and we can make a compromise between readability and need for scrolling by setting a 'line-height' somewhere between 1.0 and the inherited 1.5. --- css/MLS-navbar-left.css | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/css/MLS-navbar-left.css b/css/MLS-navbar-left.css index 57e115a43..e9308fedb 100644 --- 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" */