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
2008-05-30 13:25:54 +00:00 · 2008-05-30 13:25:54 +00:00 · b8d52932ef
commit b8d52932ef
parent 34f239498b
1 changed files with 4 additions and 0 deletions
--- 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;