diff options
| -rwxr-xr-x | buildtools/makeman | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/buildtools/makeman b/buildtools/makeman index bcc65cff..9b2653bf 100755 --- a/buildtools/makeman +++ b/buildtools/makeman @@ -51,9 +51,7 @@ def makeman(name, file, indoc): # Protect escapes before we try generating font changes. indoc = indoc.replace("\\", r"\e") # Header-bashing - indoc = indoc.replace('<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.1//EN" "DTD/xhtml11.dtd">', "") - indoc = indoc.replace('<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">', "") - indoc = indoc.replace('<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 3.2//EN">\n',"") + indoc = re.sub('(?i)<!DOCTYPE html[^>]*>', "", indoc) indoc = indoc.replace('<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">', "") indoc = indoc.replace('<meta http-equiv="Content-Type" content="text/html; charset=us-ascii"/>', "") indoc = indoc.replace('<?xml version="1.1" encoding="iso-8859-1" ?>\n',"") |