class output_filter :io_obj_channel -> out_obj_channel ->
out_obj_channel
An output_filter
filters the data written to it through the
io_obj_channel
(usually a pipe
), and writes the filtered data
to the passed out_obj_channel
.
If the filter is closed, the io_obj_channel
will be closed, too,
but not the destination out_obj_channel
(so you can still append
further data).