reactivated 'make doc' (on Linux only) with old standalone makefiles