Note: The height change probably occurs when the terminal title is set (perhaps even set again to its previous value). If the title is set via bash's PS1 then it might set it again on each keypress (but keys pressed e.g. after a "cat" won't change the window size).
On Wed, Aug 17, 2016 at 11:04 AM, Egmont Koblinger <egm...@gmail.com> wrote: > Probably relevant: https://bugzilla.gnome.org/show_bug.cgi?id=769898 >
