tree d557613e147874cfadab23223b412fd571d6ddbc
parent 34fda50beed954b3fa392297c34c9417a81d7a38
author Tom Tromey <tom@tromey.com> 1640891818 -0700
committer Tom Tromey <tom@tromey.com> 1641407793 -0700

Use filtered output in some dumping commands

There are several commands that may optionally send their output to a
file -- they take an optional filename argument and open a file.  This
patch changes these commands to use filtered output.  The rationale
here is that, when printing to gdb_stdout, filtering is appropriate --
it is, and should be, the default for all commands.  And, when writing
to a file, paging will not happen anyway (it only happens when the
stream==gdb_stdout), so using the _filtered form will not change
anything.