Different versions of man2html generated slightly different output. This change
supports both known varieties of output.