Doxygen janitor. No other changes.