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

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>