<div dir="ltr">I'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'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"><<a href="mailto:asr@eafit.edu.co" target="_blank">asr@eafit.edu.co</a>></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"><<a href="mailto:pepijn.kokke@gmail.com" target="_blank">pepijn.kokke@gmail.com</a>></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>