#! /usr/bin/env python3 import os def redirect_url(dirname, filename): # Use a path which is relative dirname = os.path.relpath(dirname) result = os.path.join( "https://www.sourceware.org/gdb", dirname, ) if filename == "index.html": # This is the default file for this directory. Omit the file, # but still end the URL with a '/'; not necessary, but helps # indicate that the target is a directory. result += "/" else: result = os.path.join(result, filename) return result def redirect_tag(dirname, filename): url = redirect_url(dirname, filename) return f'' def fixup(dirname, filename): file_path = os.path.join(dirname, filename) with open(file_path, 'rb') as f: contents = f.read() redirect_inserted_p = False with open(file_path, "wb") as f: for line in contents.splitlines(keepends=True): f.write(line) if not redirect_inserted_p and b"" in line.lower(): f.write(redirect_tag(dirname, filename).encode()) f.write(b"\n") redirect_inserted_p = True for dirname, _, files in os.walk("."): for filename in files: _, filename_ext = os.path.splitext(filename) if filename_ext.lower() not in (".htm", ".html"): # Not an HTML file, keep going. continue if os.path.join(dirname, filename) == "./bugs/index.html": # Already converted. Skip. continue fixup(dirname, filename)