Makarius wrote:
I am working with named pipes to output large amounts of text to an external process. Looking at the sources of basis/TextIO.sml etc. I've got the impression that pipes are always line-buffered. Is there an easy way to get block-buffering?
Currently TextIO.openOut sets line buffering for terminals, pipes and devices. Looking at the Basis Library document it seems that the stream should be block buffered unless it's a terminal so I'll change this.
In the meantime you can of course use TextIO.StreamIO.setBufferMode(TextIO.getOutstream f, IO.BLOCK_BUF); David _______________________________________________ polyml mailing list [email protected] http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
