Manuel points out that if printf needs a flush to act like dprintf, the result
is bigger.  Revert last patch.

1 file changed