export const DEFAULT_TERMINAL_FONT_SIZE = 10;export const TERMINAL_FONT_SIZE_STEP = 0.5;export const MIN_TERMINAL_FONT_SIZE = 6;export const MAX_TERMINAL_FONT_SIZE = 14; export function normalizeTerminalFontSize(value: number | null | undefined): number {  if (typeof value !== "number" || !Number.isFinite(value)) {    return DEFAULT_TERMINAL_FONT_SIZE;  }   return Math.min(MAX_TERMINAL_FONT_SIZE, Math.max(MIN_TERMINAL_FONT_SIZE, value));}