[Agda] Re: URLs in comments

N. Raghavendra raghu at hri.res.in
Wed Apr 8 16:27:27 CEST 2015


At 2015-04-08T12:04:01+01:00, gallais wrote:

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

Thanks!  I'll use a Makefile to post-process the HTML output with sed.

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