This ensures that classes that inherit from these have their destructors
called even if they are deleted with a pointer to the base class.
Though at the moment, this just silences a warning.
This time with more manual checking and using git blame -M -C, so that
a few cases of copied code get a copyright notice corresponding to
their initial introduction.