[Agda] How to get rid of warning

Andreas Abel abela at chalmers.se
Sat Dec 16 18:00:33 CET 2017


Mmh, are you sure it is not in any of your emacs configuration files, like

   .emacs
   .emacs.d/init.el

or other configuration files along that line, or any file you include?


On 16.12.2017 12:06, Martín Hötzel Escardó wrote:
> 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.
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda


-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www.cse.chalmers.se/~abela/


More information about the Agda mailing list