tree cd568f167395a54122b29169a32061538fec982c
parent 9fbf7f083e21263b0a0e1f76d615adaa4e13cfe5
author Tom Tromey <tom@tromey.com> 1641149739 -0700
committer Tom Tromey <tom@tromey.com> 1648579585 -0600

Rename fprintf_symbol_filtered

fprintf_symbol_filtered is misnamed, because whether filtering happens
is now up to the stream.  This renames it to fprintf_symbol, which
isn't a great name (the first "f" doesn't mean much and the second one
is truly meaningless here), but "print_symbol" was already taken.