[Agda] links in generated html files

[Wojciech Jedynak]

2011/12/8 Ramana Kumar <rk436 at cam.ac.uk>:
> 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>?

The line: (from the original file)
  List.groupBy ((==) `on` fst) $
 groups together all consecutive characters with the same MetaInfo, so
 the result is
 <a href=blah>Foo.Bar</a>

 --
 W.Jedynak