> On 10 Dec 2021, at 14:29, Rasmus Villemoes wrote:
>
> On 10/12/2021 14.08, Olivier Hainque wrote:
>> Hello,
>>
>> The attached patch is the one originally sent by Rasmus at
>>
>> https://gcc.gnu.org/pipermail/gcc-patches/2018-October/508026.html. (*)
>>
>> and which escaped the radar at
On 10/12/2021 14.08, Olivier Hainque wrote:
> Hello,
>
> The attached patch is the one originally sent by Rasmus at
>
> https://gcc.gnu.org/pipermail/gcc-patches/2018-October/508026.html. (*)
>
> and which escaped the radar at the time.
>
> The change looked good and turned out helpful in the
