Community
Participate
Working Groups
This is not strictly a Workbench issue... I have counted no less than 4 different preference pages in which I can set the font of different editors, consoles, ... I would not be surprised if there are more. Since normal users experience at least 2-3 of these editors, consoles, ... shouldn't there be one place to go and find out the default font? If individual plugins want to allow their editors to have different fonts, they can still allow people to set it but if the user does not, the UI default should take effect. NOTES:
PRODUCT VERSION: 114
Obsolete.