From 61f344920d8c155d75d0f1caf06bbb16f8532946 Mon Sep 17 00:00:00 2001 From: Jens Axel Soegaard Date: Sat, 25 Aug 2007 19:08:33 +0000 Subject: [PATCH] Merged online HelpDesk into /collects/help Most non-manual help desk pages are now in /help/servlets/home.ss Servlets are now x-expr based instead of string based. See instructions in /help/launch.ss if you want to try the online version. svn: r7160 original commit: 6d8b8a339061c975638b5799f06cebec16699742 --- collects/help/private/search.ss | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/collects/help/private/search.ss b/collects/help/private/search.ss index 8dcf76c6..5ef5af16 100644 --- a/collects/help/private/search.ss +++ b/collects/help/private/search.ss @@ -68,7 +68,7 @@ (set! doc-names (append std-doc-names - (map (lambda (s) (format "the ~a" s)) + (map (lambda (s) (format "the ~a collection" s)) txt-doc-names))) (set! doc-kinds (append (map (lambda (x) 'html) std-docs) (map (lambda (x) 'text) txt-docs)))