diff --git a/collects/scribblings/main/private/make-search.ss b/collects/scribblings/main/private/make-search.ss index 6734304f19..febbf4d407 100644 --- a/collects/scribblings/main/private/make-search.ss +++ b/collects/scribblings/main/private/make-search.ss @@ -155,7 +155,7 @@ +'