diff options
| author | Dmitry Torokhov <dmitry.torokhov@gmail.com> | 2025-11-18 10:16:55 +0300 |
|---|---|---|
| committer | Dmitry Torokhov <dmitry.torokhov@gmail.com> | 2025-11-18 10:16:55 +0300 |
| commit | f39b6c468c52745dbca9a842d91c8373fda208ab (patch) | |
| tree | 67321e90bba55fcc0f3a05f3bd9abad449b2c030 /tools/docs/gen-redirects.py | |
| parent | e08969c4d65ac31297fcb4d31d4808c789152f68 (diff) | |
| parent | 6a23ae0a96a600d1d12557add110e0bb6e32730c (diff) | |
| download | linux-f39b6c468c52745dbca9a842d91c8373fda208ab.tar.xz | |
Merge tag 'v6.18-rc6' into for-linus
Sync up with the mainline to bring in definition of
INPUT_PROP_HAPTIC_TOUCHPAD.
Diffstat (limited to 'tools/docs/gen-redirects.py')
| -rwxr-xr-x | tools/docs/gen-redirects.py | 54 |
1 files changed, 54 insertions, 0 deletions
diff --git a/tools/docs/gen-redirects.py b/tools/docs/gen-redirects.py new file mode 100755 index 000000000000..6a6ebf6f42dc --- /dev/null +++ b/tools/docs/gen-redirects.py @@ -0,0 +1,54 @@ +#! /usr/bin/env python3 +# SPDX-License-Identifier: GPL-2.0 +# +# Copyright © 2025, Oracle and/or its affiliates. +# Author: Vegard Nossum <vegard.nossum@oracle.com> + +"""Generate HTML redirects for renamed Documentation/**.rst files using +the output of tools/docs/gen-renames.py. + +Example: + + tools/docs/gen-redirects.py --output Documentation/output/ < Documentation/.renames.txt +""" + +import argparse +import os +import sys + +parser = argparse.ArgumentParser(description=__doc__, formatter_class=argparse.RawDescriptionHelpFormatter) +parser.add_argument('-o', '--output', help='output directory') + +args = parser.parse_args() + +for line in sys.stdin: + line = line.rstrip('\n') + + old_name, new_name = line.split(' ', 2) + + old_html_path = os.path.join(args.output, old_name + '.html') + new_html_path = os.path.join(args.output, new_name + '.html') + + if not os.path.exists(new_html_path): + print(f"warning: target does not exist: {new_html_path} (redirect from {old_html_path})") + continue + + old_html_dir = os.path.dirname(old_html_path) + if not os.path.exists(old_html_dir): + os.makedirs(old_html_dir) + + relpath = os.path.relpath(new_name, os.path.dirname(old_name)) + '.html' + + with open(old_html_path, 'w') as f: + print(f"""\ +<!DOCTYPE html> + +<html lang="en"> +<head> + <title>This page has moved</title> + <meta http-equiv="refresh" content="0; url={relpath}"> +</head> +<body> +<p>This page has moved to <a href="{relpath}">{new_name}</a>.</p> +</body> +</html>""", file=f) |