Thom Brown wrote: > 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.
If we are using Javascript, why can't we probe the font size and do something reasonable, e.g. make monospace larger only if it smaller than proportional? -- Bruce Momjian <br...@momjian.us> http://momjian.us EnterpriseDB http://enterprisedb.com + It's impossible for everything to be true. + -- Sent via pgsql-docs mailing list (pgsql-docs@postgresql.org) To make changes to your subscription: http://www.postgresql.org/mailpref/pgsql-docs
