http://gcc.gnu.org/bugzilla/show_bug.cgi?id=53378
--- Comment #8 from Eric Botcazou <ebotcazou at gcc dot gnu.org> 2012-05-23 18:51:55 UTC --- > Isn't that the same trick? It's just that taskLib.h is not in GCC sources so > I > can't just put the change in. The trick should be in libgcc/config/vxlib.c of course...