From 347b8bee28f71c2ceac9f519b9886cf7fefac8c7 Mon Sep 17 00:00:00 2001 From: Eli Barzilay Date: Wed, 28 May 2008 18:58:25 +0000 Subject: [PATCH] downcase index entries svn: r10007 --- collects/scribblings/main/private/make-search.ss | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/collects/scribblings/main/private/make-search.ss b/collects/scribblings/main/private/make-search.ss index 9582481c62..c1f0401607 100644 --- a/collects/scribblings/main/private/make-search.ss +++ b/collects/scribblings/main/private/make-search.ss @@ -49,9 +49,10 @@ ;; (and (exported-index-desc? desc) ;; (list (exported-index-desc-name desc) ;; (exported-index-desc-from-libs desc))) + ;; Note: using ~s to have javascript-quoted strings (format "~a[~s, ~s, ~s]" (if (eq? i (car l)) "" ",\n") - (string-join texts " ") + (string-downcase (string-join texts " ")) href html))) @script[#:noscript @list{Sorry, you must have JavaScript to use this page.}]{