[Agda] --html

[Ulf Norell]

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