https://gcc.gnu.org/bugzilla/show_bug.cgi?id=124975
Paul Thomas <pault at gcc dot gnu.org> changed:
What |Removed |Added
----------------------------------------------------------------------------
Status|NEW |RESOLVED
Resolution|--- |FIXED
--- Comment #11 from Paul Thomas <pault at gcc dot gnu.org> ---
(In reply to Paul Thomas from comment #6)
....snip...
>
> I will take care of it later this morning.
>
"This morning" lasted rather longer than intended! Sorry about that.
Pushed and backported as obvious. Closing.
Thanks,David
Paul