Support building documentation in any build directory

Currently, building documentation only works if the build directory is a subdirectory of the source directory.

Using a build directory on /var/scratch and sources in your home directory thus does not work.

This MR removes the assumptions on the location of the build directory.