help.html: make search box bigger

diff --git a/basis/help/html/stylesheet.css b/basis/help/html/stylesheet.css
index 7fe0ca3900585178c1219be37cbd0ab7ea5e1b01..e2ebeec45829b260295eb6c4375305c3cae19973 100644 (file)
--- a/basis/help/html/stylesheet.css
+++ b/basis/help/html/stylesheet.css
@@ -57,6 +57,12 @@ nav img {
     vertical-align: middle;
 }
 
+nav input {
+    padding: 3px;
+    margin-top: 0px;
+    margin-bottom: 0px;
+}
+
 .page {
     max-width: 800px;
     position: relative;