[Agda] Failed to find source of module

[Sergei Meshveliani]

On Mon, 2017-02-13 at 16:49 +0300, Sergei Meshveliani wrote:
> Dear Agda developers,
> 
> when I set to the directory  ~/mySource/Foo/  the file  TT.agda,  with
> the heading
> 
>   module TT where
> 
> (instead of the correct  module Foo.TT where),
> Agda 2.5.2 reports
> 
>  (*)   Failed to find source of module  ...
> 
> And it lists the directory names where it searched, and the directory
> ~/mySource  is not listed.


I need to add:  this report concerns the modules imported by  TT. 
 

> If I improve the name to  Foo.TT,  then it searches where it is needed.
> 
> And the error report (*) looks as misleading.
> 
> Regards,
> 
> ------
> Sergei
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>