[Agda] How to get rid of warning

Martín Hötzel Escardó m.escardo at cs.bham.ac.uk
Sat Dec 16 12:06:03 CET 2017


How do I get rid of this warning?

"
Warning (agda2): Note that the variable agda2-include-dirs is
no longer used. You may want to update your configuration. You
have at least two choices:
* Use the library management system.
* Set the include path using agda2-program-args.

One way to avoid seeing this warning is to make sure that
agda2-include-dirs is not bound.
Warning (agda2): Note that the variable agda2-include-dirs is
no longer used. You may want to update your configuration. You
have at least two choices:
* Use the library management system.
* Set the include path using agda2-program-args.

One way to avoid seeing this warning is to make sure that
agda2-include-dirs is not bound.
"

I don't want to use any library, mine or somebody else's.

I don't have a .agda directory, deliberately. (In another computer, I 
have it, with the path files empty, but I still get the above warning.)

This variable "agda2-include-dirs" is not in my .emacs. Where is it? How 
do I "update my configuration" to get rid of this warning?

Thanks.


More information about the Agda mailing list