On 8/8/08 6:22 PM, Richard Guenther wrote: > Diego, do you have any problems with that? No, thanks for fixing this. I don't think this needs changes in the documentation, but could you check? (I'm not back for another week or so). Diego.