[Agda] links in generated html files

[Nils Anders Danielsson]

On 2011-11-22 22:44, Ramana Kumar wrote:
> I presume this http://www.cse.chalmers.se/~nad/listings/lib/README.html
> was generated with agda --html.
>
> Why are the dots in module paths not included in the link text?

The generation of jump-to-definition links uses Agda's so-called
abstract and internal syntaxes. The syntax trees contain information
about the positions/ranges of names, but the dots are thrown away at an
earlier stage.

Feel free to report this issue on the bug tracker (preferably together
with a patch).

-- 
/NAD