This makes doc building more expensive (because it effectively get
built *twice*), but has the advantage of calling make in all modules, so that
auxiliary pieces of documentation (e.g., DB schemes) are guaranteed to be built
as well.

It also makes sure that everyone who wants to build the global doc has all the
needed dependencies, avoiding inconsistent builds by different people that step
on each other toes.