The previously choosen PDF file name conflicts in some repos with the
project logos (badge). Thus change https://review.opendev.org/679777
renames the desired PDF name to be doc-PROJECT.pdf to allow using the
badge in PDF files.
Follow this rename.
Change-Id: I6fbddc841039a9a66998b4ca7ae81742852d12ae