[Agda] [ANNOUNCE] Agda 2.5.1

[Andrew Pitts]

On 20 April 2016 at 18:12, Ulf Norell <ulf.norell at gmail.com> wrote:
> 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.

oh yes, I see. Thanks (and thanks for not saying RTFM!)

Andy