2009/8/19 Art Hunkins <abhunkin(a)uncg.edu>:
1) With regard to the new user controls (bigger and smaller) in the
Control
Panel (or elsewhere):
If I specify (in my script), e.g., set.property("gtk-font-name",
"14")
will "bigger" be an increment up from "14", or one up from whatever
the
default font size was?
It will always be size 14, which is about 14/72" in size.
The idea is that activity developers don't specify font sizes other
than using the default and, if they need to, <big> and <small>, so
they wouldn't do something like the above except for exceptional
cases. You may choose to be an exceptional case..
Daniel