help.html: fix nav header padding

diff --git a/basis/help/html/html.factor b/basis/help/html/html.factor
index 4708a3d0b57aa2cc784f78a800323e57885bd461..f2bd621e40c769089d3f27abb64fb01960161c53 100644 (file)
--- a/basis/help/html/html.factor
+++ b/basis/help/html/html.factor
@@ -170,10 +170,10 @@ M: pathname url-of
     dup [
         [ ".a" head? ] [ "#f4efd9;" subseq-of? ] bi and
     ] find [
-        "padding: 10px;" "padding: 0px;" replace
+        "padding: 5px;" "" replace
         "background-color: #f4efd9;" "" replace
         "}" ?tail drop
-        " border-bottom: 1px dashed #d5d5d5; width: 100%; padding-top: 15px; padding-bottom: 10px; }"
+        " border-bottom: 1px dashed #d5d5d5; width: 100%; padding-top: 10px; padding-bottom: 10px; }"
         append swap pick set-nth {
             ".a a { color: black; font-size: 24pt; line-height: 100%; }"
             ".a * a { color: #2a5db0; font-size: 12pt; }"