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

[Ulf Norell]

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/3ec47dfc/attachment.html