On 12/4/18 11:56 AM, Nick Clifton wrote: > OK, revised (v5) patch attached. Is this version acceptable to all ? Looks good to me. Independently, do you see a reason not to disable the old demangler entirely? Jason