[Agda] URLs in comments

N. Raghavendra raghu at hri.res.in
Tue Apr 7 21:32:17 CEST 2015


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.

-- 
N. Raghavendra <raghu at hri.res.in>, http://www.retrotexts.net/
Harish-Chandra Research Institute, http://www.hri.res.in/



More information about the Agda mailing list