Warning: I do not Mate is beyond hearing about it here. In any terminal (except for xterm) I use over the last half decade for sure - you can change font size the same way as in browsers Ctrl+mouse scroll wheel or by Ctrl+'+' or Ctrl+'-' if you need it for context or to show something to someone with great eyesight....
Best, T > >
