<div dir="ltr">I&#39;m also in favour of the first solution. Using double extensions is not really standard practice and might confuse both users and tools. Also, it sounds like inferring the format won&#39;t be that hard.<div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Sun, Oct 12, 2014 at 11:51 PM, Andrés Sicard-Ramírez <span dir="ltr">&lt;<a href="mailto:asr@eafit.edu.co" target="_blank">asr@eafit.edu.co</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr"><div class="gmail_extra"><span class=""><br><div class="gmail_quote">On 12 October 2014 06:28, Pepijn Kokke <span dir="ltr">&lt;<a href="mailto:pepijn.kokke@gmail.com" target="_blank">pepijn.kokke@gmail.com</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Try to infer the literate format from the file, making it explicit with Agda command-line arguments if necessary. </blockquote></div><br></span>+1<span class="HOEnZb"><font color="#888888"><br><br clear="all"><br>-- <br><div dir="ltr">Andrés<br></div>
</font></span></div></div>
<br>_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
<br></blockquote></div><br></div>