gdb/129: Re-do GDB's output pager.

[ac131313 at cygnus dot com]

>Number:         129
>Category:       gdb
>Synopsis:       Re-do GDB's output pager.
>Confidential:   no
>Severity:       non-critical
>Priority:       low
>Responsible:    unassigned
>State:          open
>Class:          change-request
>Submitter-Id:   net
>Arrival-Date:   Fri Jul 06 19:58:07 PDT 2001
>Closed-Date:
>Last-Modified:
>Originator:     ac131313@cygnus.com
>Release:        unknown-1.0
>Organization:
>Environment:

>Description:
Re-do GDB's output pager.

GDB's output pager still relies on people correctly using *_filtered
for gdb_stdout and *_unfiltered for gdb_stdlog / gdb_stderr.
Hopefully, with all normal output going to gdb_stdout, the pager can
just look at the ui_file that the output is on and then use that to
decide what to do about paging.  Sounds good in theory.
>How-To-Repeat:

>Fix:

>Release-Note:
>Audit-Trail:
>Unformatted: