[Agda] [ANNOUNCE] Agda 2.5.1

[Ulf Norell]

No, include takes a path (corresponding to -i). In this case you want to
depend on a named library, which is what the --library flag does.

/ Ulf

On Wed, Apr 20, 2016 at 5:50 PM, Andrew Pitts <Andrew.Pitts at cl.cam.ac.uk>
wrote:

> On 20 April 2016 at 14:48, Ulf Norell <ulf.norell at gmail.com> wrote:
> > Unless you have multiple Agda files needing different libraries in the
> same
> > directory, the suggested way to do this is adding a .agda-lib file with a
> > 'depend:' field to the directory (or a parent directory) containing the
> > code.
>
> Don’t you mean an `include:’ field rather than a `depend:’ field?
>
> Andy
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160420/4a342dfd/attachment.html