<div dir="ltr"><div>Thanks, I managed to get the new system working. It seems like this could save me a lot of time, so thanks for the addition!<br><br></div>Jesper<br></div><div class="gmail_extra"><br><div class="gmail_quote">On Mon, Oct 5, 2015 at 4:01 PM, Ulf Norell <span dir="ltr"><<a href="mailto:ulf.norell@gmail.com" target="_blank">ulf.norell@gmail.com</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">Yeah, I'm changing things up a bit. You should be able to use program args and -iDIR in the same way as include dirs. But please go ahead a try the new library management system (work in progress). See <a href="https://github.com/agda/agda/blob/master/doc/release-notes/2-4-4.txt#L18-L82" target="_blank">https://github.com/agda/agda/blob/master/doc/release-notes/2-4-4.txt#L18-L82</a>.<div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><div class="gmail_quote"><span class="">On Mon, Oct 5, 2015 at 2:34 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></span><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div><div class="h5"><span>On 5 October 2015 at 07:01, Jesper Cockx <<a href="mailto:Jesper@sikanda.be" target="_blank">Jesper@sikanda.be</a>> wrote:<br>
</span><span>> While working with Agda in Emacs, I usually switch include directories by<br>
> editing "Agda2 include dirs" in the Agda2 group, but after installing the<br>
> latest development agda I cannot find this entry any more.<br>
<br>
</span>The `agda2-include-dirs` variable was removed from the Emacs mode<br>
<br>
<a href="https://github.com/agda/agda/commit/94373a2221bc1ee6e3b4a8a46b8201b5a4b6e267" rel="noreferrer" target="_blank">https://github.com/agda/agda/commit/94373a2221bc1ee6e3b4a8a46b8201b5a4b6e267</a><br>
</div></div><div><div><br><span class="HOEnZb"><font color="#888888">
<br>
--<br>
Andrés<br>
_______________________________________________<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" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</font></span></div></div></blockquote></div><br></div>
</blockquote></div><br></div>