https://gcc.gnu.org/bugzilla/show_bug.cgi?id=123004
--- Comment #3 from Antoni <antoyo at gcc dot gnu.org> --- The commit was merged: https://gcc.gnu.org/git/?p=gcc.git;a=commit;h=6c565e9b32bc1e95aa2ec869285d9f51b3c45f96 (I forgot to add the PR number in the commit.)
