http://gcc.gnu.org/bugzilla/show_bug.cgi?id=42368 --- Comment #2 from charlet at adacore dot com <charlet at adacore dot com> 2011-02-09 07:43:15 UTC --- > Ping on this. Would a patch be OK? Depending on the patch, yes.