diff --git a/collects/scribblings/main/private/search.js b/collects/scribblings/main/private/search.js index f08f2b072b..26e0d180bb 100644 --- a/collects/scribblings/main/private/search.js +++ b/collects/scribblings/main/private/search.js @@ -66,8 +66,9 @@ function InitializeSearch() { +' font-family: arial, sans-serif; margin: 0em 0em 1em 0em;' +' padding: 0.5em; background-color: #f0f0f0;">' +'