Re: Bug report and whishlist

[Ethan M. <merritt@u.washington.edu>]

> Robert Hart <en...@no...> wrote:
> > 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?

-- 
Ethan A Merritt       merritt@u.washington.edu
Biomolecular Structure Center
Mailstop 357742
University of Washington, Seattle, WA 98195