Add a missing virtual destructor.

Probably harmless, I don't think we destroy these objects through pointers of
that type, but let's make sure.