+/** This class does no deletion of the pointers, but it knows how to
+ copy itself (shallow copy). We could have derived it from List<T>,
+ but this design saves a lot of code dup; for all PointerLists in the
+ program only one parent List<void*> is instantiated. */