Re: help exit

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

I propose this text:


  The commands `exit` and `quit`, as well as the END-OF-FILE character
  (usually  Ctrl-D) terminate input from the current input stream: terminal
  session,  pipe, and file input (pipe).

  If input streams are nested (inherited `load` scripts), then reading will
  continue in the parent stream. When the top level stream is closed, the
  program itself will exit.

  See "help batch/interactive" for more details.

  Each of these commands will clear the output device (as does the `clear`
  command) before exiting.


BUT: Is the last point right??? Definitely not for -persist option!

---
PM