allow floating point font size

[cipitaua]

sometimes (e.g. widgets in the status bar) the integer step from one font size to the next is too large, one would need to fine tune the font size using (one or more) decimal digits.

allowing a floating point number in the 'font size' field would help in those situations