Support decimal/floating-point values for terminal.integrated.fontSize

[ayush-that]

The editor.fontSize setting supports decimal values (e.g., 11.25, 13.5), but terminal.integrated.fontSize only accepts whole numbers. Setting a decimal value like 11.25 gets truncated to 11.

Current Behavior

{
  "editor.fontSize": 11.25,
  "terminal.integrated.fontSize": 11.25
}

The editor renders at 11.25px, but the terminal gets truncated to 11px.

Expected Behavior

terminal.integrated.fontSize should support decimal values just like editor.fontSize.

Use Case

Sometimes the difference between 11 and 12 is too significant. A value like 11.5 would provide better fine-tuning for readability, especially on high-DPI displays.

Notes

• The setting schema already defines type: 'number' (not 'integer')
• xterm.js (the terminal renderer) already supports floating-point font sizes
• This was added for editor.fontSize in Support floating point values for font size #10301 (August 2016)

I'd like to work on this. Is this something you'd accept a PR for?