Closed LisaAlmarode closed 1 year ago
I put the default font names in the preferences file. That's a nice convenience.
but then the font name is not actually used anyway!
In my experiments, the font name seems to be respected. Could you copy/paste your preferences settings that aren't being respected? Here are two examples:
The font: and textFont: preferences allowed spaces in the name but did not properly use the entire name from the file when setting the font. Fixed.
I saw some funny behavior where both font setting menu items set the system font, and the debugger did not retain text font that was set dynamically. These issues don't reproduce for what I think are combinations involving spaces... but I shall be alert.
Followup after issue #805. Things are much better.
But the settings dialog change. First, I don't actually like having to include the font name in the preferences file, when I don't know what font is the default and don't really care. I would be better if the preferences file included the specific default values (unless this is system-specific?)
legal values are font name plus font point size
font:
textFont:
So I figure something out, and enter a font name, but then the font name is not actually used anyway! I've tried both font names with spaces (which presumably need single quotes) and without, and while it will apply the pointSize, the font is always the same sans-serif one. If there is some magic syntax, that needs to be in the preferences file.