[Newbies] Preference #menuTitleBorderWidth does nothing?

[Petr Fischer]

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 at lists.squeakfoundation.org
> http://lists.squeakfoundation.org/mailman/listinfo/beginners
>