errexit inconsistent behaviour with pipelines

[Marcin Owsiany]

Hello,

I have these three very simple scripts. The only difference between them is the 
penultimate line of each of them:

| $ head -n 6 just_pipe just_for_loop pipe_and_for_loop 
| ==> just_pipe <==
| set -e
| trap 'echo aborted in line $LINENO' ERR
| echo start
| true | false
| echo ended successfully
| 
| ==> just_for_loop <==
| set -e
| trap 'echo aborted in line $LINENO' ERR
| echo start
| for a in 1; do false; done
| echo ended successfully
| 
| ==> pipe_and_for_loop <==
| set -e
| trap 'echo aborted in line $LINENO' ERR
| echo start
| true | for a in 1; do false; done
| echo ended successfully


I expected that if a simple pipeline failure causes the shell to exit, and a 
simple for loop failure causes it to exit, then a failure in their combination 
would also cause an exit. However it is not so.

| $ for script in just_pipe just_for_loop pipe_and_for_loop ;do echo -n "script 
$script: ";bash $script;done
| script just_pipe: start
| aborted in line 4
| script just_for_loop: start
| aborted in line 4
| script pipe_and_for_loop: start
| ended successfully
| $

This is using bash 3.2-0ubuntu11.

I found a workaround for a similar (same?) problem in the archive:
http://groups.google.com/group/gnu.bash.bug/browse_thread/thread/5f84f1f50b4715ae/0d8283b2c2025dc0?lnk=gst&q=errexit#0d8283b2c2025dc0

However isn't this inconsistency a bug? I also tried this in dash and zsh, and 
they both exit consistently.

regards,

Marcin
-- 
Marcin Owsiany <marcin@owsiany.pl>              http://marcin.owsiany.pl/
GnuPG: 1024D/60F41216  FE67 DA2D 0ACA FC5E 3F75  D6F6 3A0D 8AA0 60F4 1216
 
"Every program in development at MIT expands until it can read mail."
                                                              -- Unknown