[Agda] URLs in comments

Nils Anders Danielsson nad at cse.gu.se
Wed Apr 8 10:51:15 CEST 2015


On 2015-04-07 21: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?

No, see issue 986:

   allow hyperlinks in "agda --html" generated files
   https://code.google.com/p/agda/issues/detail?id=986

-- 
/NAD


More information about the Agda mailing list