<html><head><meta http-equiv="Content-Type" content="text/html charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class="">Hi, everyone.<div class=""><br class=""><div><blockquote type="cite" class=""><div class="">On Apr 20, 2016, at 5:14 AM, Andrew Pitts <<a href="mailto:Andrew.Pitts@cl.cam.ac.uk" class="">Andrew.Pitts@cl.cam.ac.uk</a>> wrote:</div><br class="Apple-interchange-newline"><div class=""><div dir="ltr" class="">On 17 April 2016 at 00:54, Andrés Sicard-Ramírez <<a href="mailto:asr@eafit.edu.co" class="">asr@eafit.edu.co</a>> wrote:<br class="">> Dear all,<br class="">><br class="">> The Agda Team is very pleased to announce the release of Agda 2.5.1.<br class=""><br class="">I have a question about the new Library management features. <br class=""><br class="">I would like to be able to specify which named library to use from within an .agda file. I hoped<br class=""><br class="">{-# OPTIONS --library=foo #-}<br class=""><br class="">would do it, but Agda says<br class=""><br class="">Unrecognized option: --library=foo<br class=""><br class="">so I guess this way of specifying a library is not possible — or did I get the syntax wrong?</div></div></blockquote><br class=""></div></div><div>I was also hoping for this. Are there any plans to add it? It would simplify things a lot.</div><div><br class=""></div><div>Best,</div><div>Harley</div></body></html>