On 2018-12-02, at 19:25, Jens Lechtenboerger wrote:

> Dear all,
>
> the attached patch allows to add a class attribute to headline
> elements in HTML export.  Is that acceptable for inclusion?

In that patch, "when" should have been "if", sorry.  Fixed version
attached.

Best wishes
Jens