On Thu, Dec 6, 2018 at 11:14 AM Jason Merrill <jason@redhat.com> wrote:
>
> Looks good to me.  Independently, do you see a reason not to disable the
> old demangler entirely?

Like so.  Does anyone object to this?  These mangling schemes haven't
been relevant in decades.