the doc changes are not ok so far. Actually WITH_DOC is for building doc with a "make" command. If you want f.ex. create only the man page you don't want to run WITH_DOC. (Background is, that manpage is shipped within the debian&ubuntu packages, and are build for every arch). But there is no need to build the rest of the documention too.