Mark Mitchell <mark@codesourcery.com> writes: [...] | When I check in this change for mainline, I will also update the 4.2 | documentation to reflect the extension being removed, and I will | update the 4.1 documentation to indicate that the feature is | deprecated. That makes sense to me. -- Gaby