quick font-scale menu (ctrl++ and ctrl+- as in web browsers)
Submitted by Stephane Chauveau
Assigned to Havoc Pennington
Description
Fonts can be changed in the profile but there is no ways to change the font in a single terminal without affecting all others terminals using the same profile.
gnome-terminal could provide a menu with a user selected list of fonts. I use this feature quite often in xterm to switch to small fonts when a shell command display very large outputs or to switch to larger fonts when I can't differenciate 0 and O anymore :-)
Another way could be to introduce a zoom factor but that would probably not work because all fonts cannot be displayed properly at all sizes.
Version: 2.0.x
Resolution: RESOLVED FIXED