[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