diff --git a/collects/scribble/scribble.css b/collects/scribble/scribble.css index 14492950..ba52b4c1 100644 --- a/collects/scribble/scribble.css +++ b/collects/scribble/scribble.css @@ -456,6 +456,10 @@ i { margin-right: 0.3em; } +.smaller{ + font-size: 82%; +} + /* A hack, inserted to break some Scheme ids: */ .mywbr { width: 0;