builtin echo buffers failed writes

[Russ Cox]

This is correct (external echo):

$ /bin/echo hello world </dev/null 1>&0
/bin/echo: write error: Bad file descriptor
$ /bin/echo goodbye world
goodbye world
$

This is not (builtin echo):

$ echo hello world </dev/null 1>&0
bash: echo: write error: Bad file descriptor
$ echo goodbye world
hello world
goodbye world
$

The second echo printed the data that failed to get
printed by the first one!

I am using the bash preinstalled on Ubuntu Gutsy.
I have not checked whether it is fixed in later versions:

$ bash --version
GNU bash, version 3.2.25(1)-release (i486-pc-linux-gnu)
Copyright (C) 2005 Free Software Foundation, Inc.
$

Russ Cox