diff --git a/collects/scribblings/main/private/search.js b/collects/scribblings/main/private/search.js index 24578fc49c..3fdf06b0f4 100644 --- a/collects/scribblings/main/private/search.js +++ b/collects/scribblings/main/private/search.js @@ -136,7 +136,7 @@ function InitializeSearch() { +" to search only the reference manual") +'>') +'' - +'