Comment 2 for bug 402116

The problem would be that python can't turn a string of "6.5" into an integer via int(). However, this works:

>>> num1 = "6.5"
>>> num2 = "6"
>>> int(float(num1))
6
>>> int(float(num2))
6
>>>

It would seem like it might be nicer in the long run to support floats for font sizes, but in the mean time the additional float() call should fix this crash.