Re: Bug report and whishlist

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

> Hmm.  That comes closer.  I don't know if that test is sufficient or not.
> What would happen in the case of "set term push" and "set term pop"?
> [I've never gotten those to work as I expect anyhow, so maybe it would
> be a small loss].

"push" remembers current terminal's name and options, and "pop" executes
"set term <oldterm> <oldopts>" as you would type it on command line.

---
PM