[Agda] --html

Ulf Norell ulfn at chalmers.se
Mon Dec 2 06:43:32 CET 2013

Not at the moment, but it does sounds like a useful feature.
Could you make a feature request on the bug tracker[*]?

/ Ulf

[*] https://code.google.com/p/agda/issues/list

On Sun, Dec 1, 2013 at 10:47 PM, Martin Escardo <m.escardo at cs.bham.ac.uk>wrote:

> I find "agda --html" very useful and I use it very often.
> Is there a way of having links to other web pages, for the
> purposes of citation, using this, similar to latex's \url{...}?
> Martin
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20131202/36dbbe18/attachment.html

More information about the Agda mailing list