[Agda] old .agdai

[Ulf Norell]

Not measurably. If there is an agdai file it will hash the source code and
compare against the hash stored in the interface file.

/ Ulf

On Mon, Apr 17, 2017 at 10:27 PM, Sergei Meshveliani <mechvel at botik.ru>
wrote:

> Dear Agda developers,
>
> when I make a change to the source  Foo.agda,  and apply the checker,
> does this make a difference for the check performance of whether
> Foo.agdai is deleted before checking or not?
>
> Thanks,
>
> ------
> Sergei
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170417/3c561796/attachment-0001.html>