Hi Joseph, > On 05 Jul 2017, at 18:09, Joseph Myers <jos...@codesourcery.com> wrote: >> Ping for patch proposed here: >> https://gcc.gnu.org/ml/gcc-patches/2017-06/msg00579.html > > This patch is OK.
Just checked-in then :) Thanks for your review! With Kind Regards, Olivier