[gps-devel] Fonts in snapshot

[Emmanuel Briot]

> 	I downloaded the last today snapshot. My preferences file contains:
>   <Src-Editor-Default-Font>terminal Medium 12</Src-Editor-Default-Font>
> 	but GPS shows "Courier Bold 10" in Edit->Preferences->Editor->Fonts&Colors 
> and does not want to change this by any means. Editor window also displays 
> with Courier instead of terminal.


This is the old format for the preferences file, and this should have
been converted automatically to the new format (something like 
   <pref name="src-editor-default-font">...</pref>
so you are probably not looking at the right preferences file