Hi,
I'd like to propose a couple of changes / enhancements to how org-export exports some data in to HTML files to make it slightly easier to style those files.
The first is re line-numbers.
At the moment those get exported as content in the HTML, although they're really additional metadata. Amongst other things, this means that if you copy/paste from the output you get the line numbers included in the text that's copied.
CSS supports arbitrary counters that can be associated with content, starting from an arbitrary value. My current hack that sort of works is the following CSS:
.....
and a change to org-html-do-format-code to wrap each line in its own <code>...</code> element:
...
;; Transcoded src line.
(format "<code>%s</code>" loc)
...
a) Does that sound reasonable?
b) Should this replace the current approach, or be an option that can be toggled by a customisation?