[PPL-devel] [GIT] ppl/ppl(master): Avoid a broken reference to another manual that is built later.