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

Reply via email to