I don't think of it as a bug but as an enhancement. If it is really easy to switch between those 2 font metrics, which one will be the default?
The one that is not compatible with Purr Data and Extended? I personally can perfectly live without that option. Salutti, Lucarda. Mensaje telepatico asistido por maquinas. ________________________________ From: Pd-list <[email protected]> on behalf of [email protected] <[email protected]> Sent: Monday, February 20, 2017 7:21 PM To: [email protected] Subject: Re: [PD] (wip) Preferences file. On 02/20/2017 07:26 PM, Jonathan Wilkes via Pd-list wrote: > Ok, if that's the case then I would suggest not to add a user-facing > font-metrics option. +1 i'd also like to add, that we should not (ever) add an option with the sole purpose of working around bugs. if you consider the slightly different font sizes a bug (and i gather you do), then we should find a solution to the bug itself (rather than provide an easy way to make everything worse). if you only consider them an annoyance, you might want to investigate in creating a gui-plugin that fixes the problem. (it seems that currently, Pd-gui signals the font metrics back to Pd-core, which will (among other things) trigger Pd-core to load it's libraries. it might be worth entangling *that*) fgamdsr IOhannes
_______________________________________________ [email protected] mailing list UNSUBSCRIBE and account-management -> https://lists.puredata.info/listinfo/pd-list
