tree 3f3fa1fd6b900ca571f3702e083ce5f35c9b5ad1
parent d53fd721a18f8c827aa69ffbd15abd99641b5e20
author Tom Tromey <tom@tromey.com> 1640550418 -0700
committer Tom Tromey <tom@tromey.com> 1641406124 -0700

Use filtered output for gdbarch dump

This changes gdbarch dumping to use filtered output.  This seems a bit
better to me, both on the principle that this is an ordinary command,
and because the output can be voluminous, so it may be nice to stop in
the middle.