<div dir="ltr">Not at the moment, but it does sounds like a useful feature.<div>Could you make a feature request on the bug tracker[*]?</div><div><br></div><div>/ Ulf</div><div><br></div><div>[*] <a href="https://code.google.com/p/agda/issues/list">https://code.google.com/p/agda/issues/list</a></div>
</div><div class="gmail_extra"><br><br><div class="gmail_quote">On Sun, Dec 1, 2013 at 10:47 PM, Martin Escardo <span dir="ltr"><<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.uk</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">I find "agda --html" very useful and I use it very often.<br>
<br>
Is there a way of having links to other web pages, for the<br>
purposes of citation, using this, similar to latex's \url{...}?<br>
<br>
Martin<br>
______________________________<u></u>_________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/<u></u>mailman/listinfo/agda</a><br>
</blockquote></div><br></div>