[Agda] links in generated html files

Ramana Kumar rk436 at cam.ac.uk
Tue Nov 22 22:44:12 CET 2011


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?
For example, in a link to Relation.Binary.On, there are actually three
separate links, one for "Relation", one for "Binary", and one for
"On".
But they all go to the same location.
This is confusing - one might expect the "Binary" part to just go to
the code for the Relation.Binary module, for example.
I think if it's supposed to be considered as one link, only one link
should appear in the html.


More information about the Agda mailing list