Man page description of delete-char, when is EOF returned?

[Parke]

Hi,

>From bash's man page:

   Commands for Changing Text
       delete-char (C-d)
              Delete  the character at point.  If point is at the beginning of
              the line, there are no characters in  the  line,  and  the  last
              character typed was not bound to delete-char, then return EOF.

I believe the above does not describe the actual behavior.  Specifically, if:

1) I bind C-d to delete-char in ~/.inputrc.
2) I press C-d at an empty prompt.
3) Then EOF is returned (and bash exits).

However in the above case, C-d (the last character typed) *is* bound
to delete-char, so according to the man page, EOF should *not* be
returned.

I believe the actual behavior is as follows:

"If point is at the beginning of the line, there are no characters in
the line and C-d is typed, then EOF is generated."

This behavior has nothing to do with delete-char, nor with what is (or
is not) bound to delete-char.  Nor does it matter what C-d is bound
to.  Even if I bind C-d to the macro "foo", bash will still exit if
the line is empty and C-d is pressed.

(Aside: I am trying to imagine a situation in which delete-char is
running and the last key typed was not bound to delete-char.  Can this
even happen?)

If I am correct and the man page description of delete-char is
inaccurate, what should change?

1) The man page
2) Bash's C-d/EOF behavior
3) Both?

I'd argue, both, but I realize others may not agree with me.  In my
case, I am binding C-d to backward-delete-char, and I want to avoid
bash exiting when I C-d (backward-delete-char) on an empty line.  (I
will kludge it with IGNOREEOF=10000, but a cleaner solution, or at
least an accurate man page, would be nicer.)

Thanks!

-Parke