<div dir="ltr"><div>I myself use the following quick&dirty sed rewriting steps in my blog-producing pipeline (for example <a href="http://gallium.inria.fr/blog/bove-reloaded/">http://gallium.inria.fr/blog/bove-reloaded/</a> ).<br><br></div> # replace markdown links<br><div> sed -i 's/\[\(.*\)\](\(.*\))/<\/a><a style="color:blue;" href="\2">\1<\/a><a class=\"Comment\">/' ./html/$@<br> sed -i 's/\[\(http.*\)\]/<\/a><a style="color:blue;" href="\1">[\1]<\/a><a class=\"Comment\">/' ./html/$@<br><br></div></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Apr 8, 2015 at 1:04 PM, gallais <span dir="ltr"><<a href="mailto:guillaume.allais@ens-lyon.org" target="_blank">guillaume.allais@ens-lyon.org</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi,<br>
<br>
A quick experiment with current agda + sed:<br>
<a href="https://gist.github.com/gallais/b29706fe7a0ee449b265" target="_blank">https://gist.github.com/<u></u>gallais/b29706fe7a0ee449b265</a><br>
<br>
The output (with no css file so it's ugly but whatever):<br>
<a href="https://rawgit.com/gallais/d167209cd1501f017e5b/raw/Url.html" target="_blank">https://rawgit.com/gallais/<u></u>d167209cd1501f017e5b/raw/Url.<u></u>html</a><span class="im HOEnZb"><br>
<br>
On 07/04/15 20:32, N. Raghavendra wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Is there a way to write URLs in comments in Agda files so that the URLs<br>
become clickable in HTML files generated from the source? Things like<br>
writing <a href="<a href="http://www.example.net/" target="_blank">http://www.example.net/</a>"<u></u>>Example</a> don't work because<br>
the entire text is enclosed in a pre element in the generated HTML.<br>
<br>
Cheers,<br>
Raghu.<br>
<br>
</blockquote>
<br></span><div class="HOEnZb"><div class="h5">
______________________________<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>
</div></div></blockquote></div><br></div>