It was merged by @antoyo as commit 54df3a3d98b521ad0652b2fe23d9132bcf77d0fa. 
Closing then. Thanks everyone! I'll send follow-ups.

--
https://forge.sourceware.org/gcc/gcc/pulls/207#issuecomment-7639

Reply via email to