File indexing completed on 2024-04-14 04:47:55

0001 #!/usr/bin/env python3
0002 
0003 import fileinput
0004 import sys
0005 import os
0006 
0007 
0008 def fix_html():
0009     for line in fileinput.input(mode='rb'):
0010         if line.lower() == b'><title\n':
0011             line = b'><meta http-equiv="content-type" content="text/html; charset=UTF-8"\n><title\n'
0012         line = line.replace(b'</TITLE', b'</title').replace(b'</title',
0013 b"""</title>
0014 <style type="text/css">
0015 body { font-family: Arial, Helvetica, sans-serif; color: #000000; background: #ffffff; }
0016 h1, h2, h3, h4 { text-align: left; font-weight: bold; color: #f7800a; background: transparent; }
0017 a:link { color: #0057ae; }
0018 pre { display: block; color: #000000; background: #f9f9f9; border: #2f6fab dashed; border-width: 1px; overflow: auto; line-height: 1.1em; }
0019 dt { font-weight: bold; color: #0057ae; }
0020 p { text-align: justify; }
0021 li { text-align: left; }
0022 .guibutton, .guilabel, .guimenu, .guimenuitem { font-family: Arial, Helvetica, sans-serif; color: #000000; background: #dcdcdc; }
0023 .application { font-weight: bold; }
0024 .command { font-family: "Courier New", Courier, monospace; }
0025 .filename { font-style: italic; }
0026 </style""")
0027         os.write(sys.stdout.fileno(), line)
0028 
0029 if __name__ == '__main__':
0030     fix_html()