installation: documentation is built as the same user as the make install target is issued
When I do:
./configure && make && sudo make install documentation is built during last command in
build/ directory. This leads to a situation, where user can't remove this directory before next build without sudo.
./configure && make && make doc && sudo make install && rm -rf buildsucceeds (and installs documentation)
./configure && make && sudo make install && rm -rf buildsucceeds (but doesn't install documentation)
@spaghettisalat do you think it is something feasible?
make install would require to check, if documentation is built. Alternatively we could make a separate target
make install_doc, but I better like the proposed approach.