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

[Andrés Sicard-Ramírez]

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