On Fri, May 10, 2019 at 05:34:48PM +0100, Gavin Smith wrote:
> On 5/10/19, Patrice Dumas wrote:
> > On Thu, May 09, 2019 at 07:13:05PM +0100, Gavin Smith wrote:
> >> I think there should be a more reliable way to identify links to
> >> index nodes from the table of contents in index.html in HTML o
On 5/10/19, Patrice Dumas wrote:
> On Thu, May 09, 2019 at 07:13:05PM +0100, Gavin Smith wrote:
>> I think there should be a more reliable way to identify links to
>> index nodes from the table of contents in index.html in HTML output.
>> Currently the only way is to check if "Index" appears in th
On Thu, May 09, 2019 at 07:13:05PM +0100, Gavin Smith wrote:
> I think there should be a more reliable way to identify links to
> index nodes from the table of contents in index.html in HTML output.
> Currently the only way is to check if "Index" appears in the name of
> the page. This would be us
You're welcome. Gavin did most of the work.
I've revised (but not yet merged) the index for the gawk manual to take
advantage of the new features, and it too looks wonderful. I'm pleased
with the new features and am glad other people are using them too.
Regards,
Arnold
Raymond Toy wrote:
> Th
