From 1f02db2dc46bbc83364c8b9340dfc386e2263ba3 Mon Sep 17 00:00:00 2001 From: Eli Barzilay Date: Sun, 6 Jul 2008 05:10:52 +0000 Subject: [PATCH] Search box has same font size as the rest of the navset, and is wider. svn: r10629 original commit: 9629528865f680dd5a1c22d5f88d026d8066332e --- collects/scribble/html-render.ss | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/collects/scribble/html-render.ss b/collects/scribble/html-render.ss index bf6a9228..de724ca6 100644 --- a/collects/scribble/html-render.ss +++ b/collects/scribble/html-render.ss @@ -194,7 +194,7 @@ [emptylabel "...search manuals..."] [dimcolor "#888"]) `(input - ([style ,(sa "font-size: 60%; margin: 0px; padding: 0px;" + ([style ,(sa "width: 16em; margin: 0px; padding: 0px;" " background-color: #eee; color: "dimcolor";" " border: 1px solid #ddd; text-align: center;")] [type "text"]