Only remove the directory contents. If the directory itself is removed,
then `sudo make install` creates a root-owned …/doc/ directory. That
breaks the next non-root build.
This was an accident of 0b1904d835.
Note: the following does not work, because it misses renamed help files
(which would no longer be in the build-tree definition)
COMMAND ${CMAKE_COMMAND} -E remove ${BUILDDOCFILES} ${GENERATED_HELP_TAGS}