<div dir="ltr"><div>I myself use the following quick&amp;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 &#39;s/\[\(.*\)\](\(.*\))/&lt;\/a&gt;&lt;a style=&quot;color:blue;&quot; href=&quot;\2&quot;&gt;\1&lt;\/a&gt;&lt;a class=\&quot;Comment\&quot;&gt;/&#39; ./html/$@<br>  sed -i &#39;s/\[\(http.*\)\]/&lt;\/a&gt;&lt;a style=&quot;color:blue;&quot; href=&quot;\1&quot;&gt;[\1]&lt;\/a&gt;&lt;a class=\&quot;Comment\&quot;&gt;/&#39; ./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">&lt;<a href="mailto:guillaume.allais@ens-lyon.org" target="_blank">guillaume.allais@ens-lyon.org</a>&gt;</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&#39;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 &lt;a href=&quot;<a href="http://www.example.net/" target="_blank">http://www.example.net/</a>&quot;<u></u>&gt;Example&lt;/a&gt; don&#39;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>