On 31 August 2010 17:57, Tom Lane <tgl@sss.pgh.pa.us> wrote:
> "Joshua D. Drake" <jd@commandprompt.com> writes:
>> On Tue, 2010-08-31 at 12:24 -0400, Tom Lane wrote:
>>> There's a reason why it was done that way before ...
>
>> There is no reason to do that. Every browser has the ability to override
>> font settings. If the user has accessibility issues, they have the
>> ability to deal with it.
>
> If that's actually the case, I withdraw the complaint. I read Thom's
> message as saying that he was overriding the user's font settings.
In a way I am. Users have the ability (although not often exercised)
to change the default font and size. I gave the HTML tag a font-size,
so that anything under it would be based on that. We use relative
font sizes in our CSS, which means usually we'd be proportional to
whatever the user had set. But what I've done is set a base size
(17px in this case, and only in documentation) which everything else
will be based on. So the downside is whatever the user set their
default font size to in their browser will be ignored (or not fallen
back to if you prefer). This doesn't, however, prevent them from
using a text zoom (available in pretty much every web browser) to
increase the size of all rendered fonts.
The problem is, by default, Firefox sets proportional fonts to 16px,
and monospace to 12px, so there's always a visual discrepancy when
these fonts appear alongside one another.
But the benefit of the javascript hack was that we weren't setting a
base font size for everything, we just bump up the relative font size
for elements which are monospaced by default.
There's pros and cons to both approaches. I'm not sure which one you
guys prefer.
--
Thom Brown
Twitter: @darkixion
IRC (freenode): dark_ixion
Registered Linux user: #516935