Re: use id="xx" instead of <a name="xx"> in html output

[Gavin Smith]

On 9 February 2016 at 20:07, Per Bothner <address@hidden> wrote:
> If we defer adding the <div>s for node until we see they needed (which may
> make sense), then we get:
>
> <section class="chapter" id="Chapter1">
> <header>LINKS for chapter1</header>
> <h2>Chapter1</h2>
> Preamble
> <table class="menu">...</table>
>
> <section class="section" id="section11">
> <header>LINKS for section11</header>
> <h3>Section11</h3>
> section11-text
> </section>
>
> <section class="section" id="section12">
> <header>LINKS for section12</header>
> <h3>Section12</h3>
> section12-text
> </section>
>
> </section>
>

I agree in principle. This would have to be optional (because
<section> is an HTML5 tag), but it would clearly be useful for
automatic processing with JavaScript. Someone has to find the time to
implement it, but that's the only barrier.