diff --git a/collects/scribblings/main/private/search.js b/collects/scribblings/main/private/search.js index 90426855f6..00601a221c 100644 --- a/collects/scribblings/main/private/search.js +++ b/collects/scribblings/main/private/search.js @@ -110,7 +110,7 @@ function InitializeSearch() { +'' +'