For information, the 16px font has now been removed, and replaced with 13px, which should make the font sizes a bit more consistent.
By the way did you keep track of where you saw these fonts? I guess some are very common, like the 13px one, but others perhaps only appear once or twice, in which case we could try to change them to something more standard.
