14 Nov
2006
14 Nov
'06
8:38 a.m.
Is time to remove unused things like #menuTitleBorderWidth? Confusing.
Thanks, pf
Petr Fischer píše v Čt 09. 11. 2006 v 21:13 +0100:
Hi,
has preference #menuTitleBorderWidth any effect? (It's used in color themes (ColorTheme) too)
Thanks, pf
Beginners mailing list Beginners@lists.squeakfoundation.org http://lists.squeakfoundation.org/mailman/listinfo/beginners