id,summary,reporter,owner,description,type,status,priority,milestone,component,version,resolution,keywords,cc
1298,Changing font in preferences is not applied to existing editors,dolmen,,"When the font is changed using the preference dialog, the new font is only applied to editors created after that change. Existing editors are not updated.",defect,closed,blocker,,Preference System,0.93,fixed,font preference,