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/