From d1c2d217215bb8cf88722e48a45c4c9856440609 Mon Sep 17 00:00:00 2001 From: John Benediktsson Date: Thu, 13 Feb 2020 21:43:24 -0800 Subject: [PATCH] help.html: tweak the navbar a bit. --- basis/help/html/html.factor | 9 +++++---- basis/help/html/stylesheet.css | 12 ++++++++++++ 2 files changed, 17 insertions(+), 4 deletions(-) diff --git a/basis/help/html/html.factor b/basis/help/html/html.factor index 0a428172cd..4105208218 100644 --- a/basis/help/html/html.factor +++ b/basis/help/html/html.factor @@ -76,11 +76,12 @@ M: pathname url-of [XML diff --git a/basis/help/html/stylesheet.css b/basis/help/html/stylesheet.css index 4d1f56375b..411de0620d 100644 --- a/basis/help/html/stylesheet.css +++ b/basis/help/html/stylesheet.css @@ -17,6 +17,12 @@ a:visited { text-decoration: none; color: #104e8b; } a:active { text-decoration: none; color: #104e8b; } a:hover { text-decoration: underline; color: #104e8b; } +input { + border: 1px solid #999999; + font-size: smaller; + border-radius: 3px; +} + .navbar { background-color: #f3f2ea; padding: 10px; @@ -24,6 +30,12 @@ a:hover { text-decoration: underline; color: #104e8b; } font: 12pt sans-serif; } +.navbar a { + border-right: 1px solid #999; + padding-right: 10px; + margin-right: 5px; +} + .page { font-size: 120%; margin: 20px;