[Agda] URLs in comments

[gallais]

Hi,

A quick experiment with current agda + sed:
https://gist.github.com/gallais/b29706fe7a0ee449b265

The output (with no css file so it's ugly but whatever):
https://rawgit.com/gallais/d167209cd1501f017e5b/raw/Url.html

On 07/04/15 20:32, N. Raghavendra wrote:
> Is there a way to write URLs in comments in Agda files so that the URLs
> become clickable in HTML files generated from the source?  Things like
> writing <a href="http://www.example.net/">Example</a> don't work because
> the entire text is enclosed in a pre element in the generated HTML.
>
> Cheers,
> Raghu.
>