CMake: optional doc target

Currently there is no way (that I can see) to disable the add_custom_target(doc ...) in the doc/CMakeLists.txt. This is problematic when using Eigen3 as a CMake add_subdirectory dependency in projects that also build their own documentation, as the target name doc will always be defined by eigen. CMake does not allow multiple targets with the same name (without falling back on the deprecated CMP0002) and there is no way to delete or replace a target.

The easiest fix would be to add an option like eg BUILD_DOC to eigen. This could be easily done in the root CMakeLists.txt by replacing the

add_subdirectory(doc EXCLUDE_FROM_ALL)

line with

option(BUILD_DOC "Enable creation of Eigen documentation" ON)
if(BUILD_DOC)
  add_subdirectory(doc EXCLUDE_FROM_ALL)
endif()

This leaves the default behaviour unchanged.