> Proposed patch below/attached. > (-w to hide indent change) See http://gcc.gnu.org/contribute.html for guidelines.
> I'll open a bug. See http://gcc.gnu.org/bugs for guidelines. Generally speaking, posting a patch inlined in a message on gcc@gcc.gnu.org will most likely result in it being lost and forgotten. In order to report an issue, please open a ticket with bugzilla. In order to submit a patch, please use gcc-patc...@gcc.gnu.org. In both cases, follow the guidelines written down in the aforementioned documentation. Thanks in advance. -- Eric Botcazou
