...producing error messages about trying to access private undefined unique_ptr
copy ctor etc.
Partial revert of 014e7933af751bfe0a03867373b82efa806f3a3d "svtools:
std::auto_ptr -> std::unique_ptr: ...changing HTMLOptions to
std::vector<std::unique_ptr<...>> because boost::ptr_vector<...>::push_back only
supports auto_ptr, not unique_ptr," going the awkward
std::unique_ptr x(...);
push_back(x.get());
x.release();
route instead (which could be simplified if boost::ptr_vector::push_back ever
started to support unique_ptr).
Change-Id: I15693030a0bbfdedbfdfbe76ede5d0c74f4e5b41
9755653991