[Agda] Development version of agda-mode doesn't recognize symlinks?

Jan Stolarek jan.stolarek at p.lodz.pl
Wed Nov 27 10:46:07 CET 2013


Is this module special in any way? It seems to have normal implementation just like any other 
module.

Janek

Dnia wtorek, 26 listopada 2013, Nils Anders Danielsson napisał:
> On 2013-11-26 13:26, Jan Stolarek wrote:
> > It seems that symlinks are confusing agda-mode. Any way to solve that
> > problem?
>
> Symlinks appear to be supported for regular modules:
>
>    $ mkdir A
>    $ ln -s A B
>    $ echo 'module A.M where' > A/M.agda
>    $ agda B/M.agda
>    Checking A.M (/tmp/A/M.agda).
>    Finished A.M.
>
> However, I guess the code that handles the new module Agda.Primitive
> breaks some invariant.




More information about the Agda mailing list