Ctrl-D exits unexpectedly

[Martin Szummer]

From: mos25@cam.ac.uk

Subject: [50 character or so descriptive subject here (for reference)]

Configuration Information [Automatically generated, do not change]:
Machine: x86_64
OS: linux-gnu
Compiler: gcc
Compilation CFLAGS:  -DPROGRAM='bash' -DCONF_HOSTTYPE='x86_64' 
-DCONF_OSTYPE='l$
uname output: Linux krakow 3.8.0-19-generic #30-Ubuntu SMP Wed May 1 
16:35:23 U$
Machine Type: x86_64-pc-linux-gnu

Bash Version: 4.2
Patch Level: 45
Release Status: release

Description:
The IGNOREEOF behavior changed in Bash 4.2 (in Ubuntu 13.04) compared to 
bash in Ubuntu 12.10.

I used to have in my .bashrc
set -o ignoreeof
export IGNOREEOF=10
and in this case, Ctrl-D would never exit the shell, even if pressed 
more than 10 times.

In the newer Bash 4.2 (patch 45), it *does* exit the shell after 10 Ctrl-D.
The bug is that set -o ignoreeof does not have an effect.
Even after unsetting IGNOREEOF, the shell exits.  The set -o ignoreeof 
by itself does not make the shell ignore EOF; the only way seems to be 
to set IGNOREEOF to a very large number.


Thanks,
   Martin