Re: [PATCH] fix PR ada/80888

[Arnaud Charlet]

> Ping
> If OK, can it be applied please?
> (patch applies cleanly to current sources)

Patch is OK. I'll apply it when I get a chance.

Arno