From b8d52932ef3183e90a70df8a91ccb390e3c7f776 Mon Sep 17 00:00:00 2001 From: Matthew Flatt Date: Fri, 30 May 2008 13:25:54 +0000 Subject: [PATCH] adjust search-page sizing of 'provided from' to use a CSS entry, which scales by the magic 82% instead of 80% (because 80% drops just below the threshold of anti-aliasing the default monospace font in Safari) svn: r10036 original commit: a78bf662b23e2395ab996fa3d0752ed2c65ebec1 --- collects/scribble/scribble.css | 4 ++++ 1 file changed, 4 insertions(+) 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;