1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/en/fixhtml.py	Fri Mar 30 23:24:03 2007 -0700
     1.3 @@ -0,0 +1,23 @@
     1.4 +#!/usr/bin/env python
     1.5 +
     1.6 +import os
     1.7 +import sys
     1.8 +import re
     1.9 +
    1.10 +unicode_re = re.compile(r'&#x00([0-7][0-9a-f]);', re.I)
    1.11 +fancyvrb_re = re.compile(r'id="fancyvrb\d+"', re.I)
    1.12 +
    1.13 +tmpsuffix = '.tmp.' + str(os.getpid())
    1.14 +
    1.15 +def fix_ascii(m):
    1.16 +    return chr(int(m.group(1), 16))
    1.17 +
    1.18 +for name in sys.argv[1:]:
    1.19 +    tmpname = name + tmpsuffix
    1.20 +    ofp = file(tmpname, 'w')
    1.21 +    for line in file(name):
    1.22 +        line = unicode_re.sub(fix_ascii, line)
    1.23 +        line = fancyvrb_re.sub('id="fancyvrb"', line)
    1.24 +        ofp.write(line)
    1.25 +    ofp.close()
    1.26 +    os.rename(tmpname, name)