From f69d5a49c30e4d2444e2f01d2e0c834eb9b3769b Mon Sep 17 00:00:00 2001 From: Eli Barzilay Date: Fri, 11 Jan 2008 02:29:49 +0000 Subject: [PATCH] remove the now-redundant main-doc option svn: r8288 original commit: fff894d7100add97eddfe8f965e7c1f558abd87c --- collects/scribblings/scribble/info.ss | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/collects/scribblings/scribble/info.ss b/collects/scribblings/scribble/info.ss index f9850b27..0ee0084b 100644 --- a/collects/scribblings/scribble/info.ss +++ b/collects/scribblings/scribble/info.ss @@ -1,4 +1,4 @@ (module info setup/infotab (define name "Scribblings: Scribble") - (define scribblings '(("scribble.scrbl" (multi-page main-doc)))) + (define scribblings '(("scribble.scrbl" (multi-page)))) (define doc-categories '(tool)))