diff --git a/collects/scribble/scribble.css b/collects/scribble/scribble.css index ede33cc3..a43c55f5 100644 --- a/collects/scribble/scribble.css +++ b/collects/scribble/scribble.css @@ -196,6 +196,14 @@ font-weight: bold; margin: 0.2em 0.2em 0.2em 0.2em; } +.sepspace { + font-size: 40%; +} + +.septitle { + font-size: 70%; +} + /* ---------------------------------------- */ /* Inherited methods, left margin */ diff --git a/collects/scribblings/scribble/info.ss b/collects/scribblings/scribble/info.ss index ddd6ca1f..7a7f6ba7 100644 --- a/collects/scribblings/scribble/info.ss +++ b/collects/scribblings/scribble/info.ss @@ -1,4 +1,3 @@ #lang setup/infotab -(define scribblings '(("scribble.scrbl" (multi-page)))) -(define doc-categories '(tool)) +(define scribblings '(("scribble.scrbl" (multi-page) (tool))))