Re: Bug report and whishlist

[Petr M. <mi...@ph...>]

> > > I guess we should only do that if the term type actually changes (rather
> > > than if just the options change).
>
> > Ethan Merritt <merritt@u.washington.edu> wrote:
> > >What would happen in the case of "set term push" and "set term pop"?
>
> On Wednesday 11 May 2005 08:31 am, Petr Mikulik wrote:
> > "push" remembers current terminal's name and options, and "pop" executes
> > "set term <oldterm> <oldopts>" as you would type it on command line.
>
> I meant, does "set term push" count as changing the terminal type for the
> purposes of Robert's proposed test?

If it works for "set term blabla" from command line or script, then it will
work for "set term pop" as well.

---
PM