Hi Jose,
On 21/04/20 16:38, Thomas Koenig wrote:Do you have commit privileges? It not, I can commit it for you.No i do not. I would be grateful if you could.
Done, as https://gcc.gnu.org/git/gitweb.cgi?p=gcc.git;h=808a6eadda1a353ce3a70556feac128580491b24 .
Thanks a lot for the patch! Regards Thomas