On Thursday 07 August 2003 13:11, Dave Page wrote:Unfortunately, Times seems to be the default browser's font...
It still seems to be writing the files to the pgadmin3 directory, not
the new cache directory.
Sorry, I did not commit to CVS and deleted my changes. Done now.
BTW, is there anything we can do about the font? The default Times New
Roman looks crap...
I would prefer no default font at all in CSS to let the operatings system or the user choose his/her preffered font. Otherwise, there can be display errors, even in Japanese (which was the case with the current stylesheet).
Where did we default Times New Roman?
Is it possible to set the font for "usual" languages to a nice one, and leave the font default for "odd" languages like Japanese?
Regards, Andreas
---------------------------(end of broadcast)--------------------------- TIP 8: explain analyze is your friend