<div dir="ltr">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).<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Aug 17, 2016 at 11:04 AM, Egmont Koblinger <span dir="ltr"><<a href="mailto:egmont@gmail.com" target="_blank">egmont@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Probably relevant: <a href="https://bugzilla.gnome.org/show_bug.cgi?id=769898" target="_blank">https://bugzilla.gnome.org/<wbr>show_bug.cgi?id=769898</a><br></div>
</blockquote></div><br></div>