[Agda] Where did "agda2 include dirs" go?

[Jesper Cockx]

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!

Jesper

On Mon, Oct 5, 2015 at 4:01 PM, Ulf Norell <ulf.norell at gmail.com> wrote:

> 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
> https://github.com/agda/agda/blob/master/doc/release-notes/2-4-4.txt#L18-L82
> .
>
> / Ulf
>
> On Mon, Oct 5, 2015 at 2:34 PM, Andrés Sicard-Ramírez <asr at eafit.edu.co>
> wrote:
>
>> On 5 October 2015 at 07:01, Jesper Cockx <Jesper at sikanda.be> wrote:
>> > While working with Agda in Emacs, I usually switch include directories
>> by
>> > editing "Agda2 include dirs" in the Agda2 group, but after installing
>> the
>> > latest development agda I cannot find this entry any more.
>>
>> The `agda2-include-dirs` variable was removed from the Emacs mode
>>
>>
>> https://github.com/agda/agda/commit/94373a2221bc1ee6e3b4a8a46b8201b5a4b6e267
>>
>>
>> --
>> Andrés
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20151005/74577633/attachment.html