Hi Joseph,
> On 05 Jul 2017, at 18:09, Joseph Myers 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
On Wed, 5 Jul 2017, Olivier Hainque wrote:
> Hello,
>
> Ping for patch proposed here:
> https://gcc.gnu.org/ml/gcc-patches/2017-06/msg00579.html
This patch is OK.
--
Joseph S. Myers
jos...@codesourcery.com
Hello,
Ping for patch proposed here:
https://gcc.gnu.org/ml/gcc-patches/2017-06/msg00579.html
Thanks much in advance,
With Kind Regards,
Olivier
> On Jun 9, 2017, at 10:42 , Olivier Hainque wrote:
>
> Hello,
>
> This is a follow-up improvement over the change
> introduced from
>
> https://