docs: add tools/docs/gen-redirects.py

Add a new script and a new documentation 'make' target,
htmldocs-redirects.

This will generate HTML stub files in the HTML documentation output
directory that redirect the browser to the new path.

Suggested-by: Konstantin Ryabitsev <konstantin@linuxfoundation.org>
Suggested-by: Jonathan Corbet <corbet@lwn.net>
Signed-off-by: Vegard Nossum <vegard.nossum@oracle.com>
Signed-off-by: Jonathan Corbet <corbet@lwn.net>
Message-ID: <20250905144608.577449-4-vegard.nossum@oracle.com>
This commit is contained in:
Vegard Nossum 2025-09-05 16:46:08 +02:00 committed by Jonathan Corbet
commit f2c2f64900
3 changed files with 61 additions and 2 deletions

View file

@ -1799,8 +1799,9 @@ $(help-board-dirs): help-%:
# Documentation targets
# ---------------------------------------------------------------------------
DOC_TARGETS := xmldocs latexdocs pdfdocs htmldocs epubdocs cleandocs \
linkcheckdocs dochelp refcheckdocs texinfodocs infodocs
DOC_TARGETS := xmldocs latexdocs pdfdocs htmldocs htmldocs-redirects \
epubdocs cleandocs linkcheckdocs dochelp refcheckdocs \
texinfodocs infodocs
PHONY += $(DOC_TARGETS)
$(DOC_TARGETS):
$(Q)$(MAKE) $(build)=Documentation $@