[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