why are *two* ctrl-D's needed with readlines()

[Wilhelm Fitzpatrick]

"Wilhelm Fitzpatrick" <rafial at w...> wrote in message
news:mailman.1002297908.5879.python-list at p...
> I was writing a little python script using
>
> for line in sys.stdin.readlines() :
>
> to iterate through input, and I noticed that I had to press ctrl-D
> TWICE to terminate input.
...
> for line in sys.stdin.read().splitlines() :
>
> terminates on the first ctrl-D (as I would expect).

"Steve Holden" <sholden at h...> responded:
> Are you pressing the ^D at the end of a line of input, or at the
> start of a blank line?

(I replied to this message once already, but I think it went to Steve
and not the list.  My apologies if some of this is a duplicate)

I am pressing ctrl-D at the start of blank line.  My platform is
indeed Linux, and that may have some bearing.  I could not reproduce
the behavior on a Solaris box with 2.1.1 installed.  I installed 2.1.1
under Linux, and got the same problem behavior as described above.

Another interesting test I did was to place a readlines() loop in a
script and invoke it this way:

cat | myscript.py

Which produced the correct behavior (EOF on single ctrl-d)
It appears to be some bad interaction between Linux (glibc?) and the
way python handles stdin for readlines(), as opposed to say read() or
raw_input(), which seem to be doing the right thing.

Any thoughts from the gurus?