| 1 | |
| 2 | |
| 3 | |
| 4 | |
| 5 | |
| 6 |
|
| 7 | |
| 8 | the output of tools/docs/gen-renames.py.
|
| 9 |
|
| 10 | Example:
|
| 11 |
|
| 12 | tools/docs/gen-redirects.py --output Documentation/output/ < Documentation/.renames.txt
|
| 13 |
|
| 14 |
|
| 15 | import argparse
|
| 16 | import os
|
| 17 | import sys
|
| 18 |
|
| 19 | parser = argparse.ArgumentParser(description=__doc__, formatter_class=argparse.RawDescriptionHelpFormatter)
|
| 20 | parser.add_argument('-o', '--output', help='output directory')
|
| 21 |
|
| 22 | args = parser.parse_args()
|
| 23 |
|
| 24 | for line in sys.stdin:
|
| 25 | line = line.rstrip('\n')
|
| 26 |
|
| 27 | old_name, new_name = line.split(' ', 2)
|
| 28 |
|
| 29 | old_html_path = os.path.join(args.output, old_name + '.html')
|
| 30 | new_html_path = os.path.join(args.output, new_name + '.html')
|
| 31 |
|
| 32 | if not os.path.exists(new_html_path):
|
| 33 | print(f"warning: target does not exist: {new_html_path} (redirect from {old_html_path})")
|
| 34 | continue
|
| 35 |
|
| 36 | old_html_dir = os.path.dirname(old_html_path)
|
| 37 | if not os.path.exists(old_html_dir):
|
| 38 | os.makedirs(old_html_dir)
|
| 39 |
|
| 40 | relpath = os.path.relpath(new_name, os.path.dirname(old_name)) + '.html'
|
| 41 |
|
| 42 | with open(old_html_path, 'w') as f:
|
| 43 | print(f"""\
|
| 44 | <!DOCTYPE html>
|
| 45 |
|
| 46 | <html lang="en">
|
| 47 | <head>
|
| 48 | <title>This page has moved</title>
|
| 49 | <meta http-equiv="refresh" content="0; url={relpath}">
|
| 50 | </head>
|
| 51 | <body>
|
| 52 | <p>This page has moved to <a href="{relpath}">{new_name}</a>.</p>
|
| 53 | </body>
|
| 54 | </html>""", file=f)
|