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