Tom Tromey d0b1020bf1 Rename print_spaces_filtered
print_spaces_filtered is now misnamed, because whether filtering
happens is up to the stream.  So, rename it.
2022-03-29 12:46:24 -06:00
..
2022-03-29 12:46:24 -06:00
2022-03-29 12:46:24 -06:00
2022-03-23 07:41:19 -04:00
2022-03-29 12:46:24 -06:00
2022-03-29 12:46:24 -06:00
2022-03-29 12:46:24 -06:00
2022-03-29 12:46:24 -06:00
2022-03-29 12:46:24 -06:00
2022-03-29 12:46:24 -06:00
2022-03-23 07:41:19 -04:00
2022-03-29 12:46:24 -06:00