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

Andrés Sicard-Ramírez asr at eafit.edu.co
Mon Oct 5 14:29:52 CEST 2015


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. Did anything
> change to how include directories are specified? I cannot find anything
> about this in the changelog.

See "Library management" (I haven't used it) in

  https://github.com/agda/agda/blob/master/doc/release-notes/2-4-4.txt

-- 
Andrés


More information about the Agda mailing list