File indexing completed on 2024-04-28 08:45:26
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()