mkhtml: apply own line numbering to highlighted sources
commitd2bec9adceb4ce3172946aba15f7b7148f191c05
authorStefan Sauer <ensonic@users.sf.net>
Mon, 19 Mar 2018 19:41:58 +0000 (19 20:41 +0100)
committerStefan Sauer <ensonic@users.sf.net>
Mon, 19 Mar 2018 19:41:58 +0000 (19 20:41 +0100)
tree09adc3bfe6948c220cf019eb37bd3d6c39ab0130
parentb77d97bfe0186eb727604dbad565dc4dde0eb273
mkhtml: apply own line numbering to highlighted sources

The one from pygments is hard to style to look the same way.
gtkdoc/mkhtml2.py