Re: print stdout and flush

[Roberto Ierusalimschy <roberto@...>]

> For those who need more control use io.stdout.write() anyway.
> So there is a good point for a flush after every print(). For those
> for which this is too much performance hit, should use write()
> instead.

That is true. BTW, io.write is also more efficient when printing numbers.

-- Roberto