[Agda] links in generated html files

[Ramana Kumar]

Thanks for doing that!
I haven't run your patch yet, but after looking at it briefly I have a
question: does the generate HTML end up like <a href=blah>Foo.Bar</a>
or like <a href=blah>Foo</a><a href=blah>.</a><a href=blah>Bar</a>?

On Thu, Dec 8, 2011 at 10:15 AM, Wojciech Jedynak <wjedynak at gmail.com> wrote:
> 2011/12/6 Nils Anders Danielsson <nad at chalmers.se>:
>> Feel free to report this issue on the bug tracker (preferably together
>  > with a patch).
>
> http://code.google.com/p/agda/issues/detail?id=539