GTK font sizes

[Ed Greshko]

On 06/18/15 11:02, Felix Miata wrote:
> UI fonts that you want to be different from system fonts need to be changed according to http://kb.mozillazine.org/Pane_and_menu_fonts or by using a Mozilla/TB theme. 

My, my don't I feel embarrassed.

This actually does work.  The system I was on actually has 2 profiles in the ~/.thunderbird directory and I modified the wrong one!

Thanks very much for your help.