[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