xref: /petsc/doc/add_man_page_redirects.py (revision 0ec0a084dafaf19d7cb029f108202517fa408668)
1""" Add redirect pages to preserve previous man page URLs """
2
3import os
4
5TEMPLATE = ('<!DOCTYPE html>\n'
6            '<html>'
7            '<head><meta http-equiv="refresh" content="0; url=%s" /></head>'
8            '<body><a href="%s">Click here</a></body>'
9            '</html>')
10
11
12def _generate_page(name, location):
13    redirect_filename = os.path.join(location, name + ".html")
14    with open(redirect_filename, "w") as redirect_file:
15        redirect_file.write(TEMPLATE % (name, name))
16
17
18def add_man_page_redirects(root):
19    """ Add redirecting .html files for all man pages.
20
21    Assumes a particular directory structure relative to root.  For each
22    subdirectory (manual page section) of root/manualpages, enumerate all
23    contained directories as names, and add links name.html which redirect to
24    name/ (from which a web server will load name/index.html).
25    """
26    manualpages_dir = os.path.join(root, "manualpages")
27    for mansec in os.listdir(manualpages_dir):
28        subdirectory = os.path.join(manualpages_dir, mansec)
29        if os.path.isdir(subdirectory):
30            for name in os.listdir(subdirectory):
31                if os.path.isdir(os.path.join(subdirectory, name)):
32                    _generate_page(name, subdirectory)
33