On 01/16/2012 05:03 PM, Sergio Durigan Junior wrote: > On Monday, January 16 2012, Tom Tromey wrote: >> I have no further comments, but I would rather Pedro give the final OK >> on this. > > Ok. Here is the final version of the patch, then. Looks good to me. Thanks. -- Pedro Alves