Gui preferences dialog font sizes

@ttl there’s a stackoverflow post about preference dialog box font sizes being too small. Where does that font size get pulled from? it doesn’t appear to be a Preferences setting. is it OS dependent?

see Change Octave Super Tiny font size - Stack Overflow

It probably is. If it is Linux, it might also depend on X server vs. Wayland and/or Desktop environment.