<div dir="ltr">Hi Sergei,<div> If you open this as an issue on the standard library issue tracker we'll try and get a fix pushed through to change the message.</div><div>Thanks,</div><div>Matthew</div></div><br><div class="gmail_quote"><div dir="ltr">On Thu, Dec 6, 2018 at 6:38 PM Sergei Meshveliani <<a href="mailto:mechvel@botik.ru">mechvel@botik.ru</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">Dear Agda team,<br>
<br>
Development library of November 9 and of December 4, 2018 <br>
both report "Installed lib-0.17".<br>
But these libraries are very different. For example, the latter has<br>
Magma, and behaves differently on my application. <br>
Is it possible for it to issue, say,<br>
"Development library of <date>" ?<br>
<br>
By the way, what is a regular tool to ask for the library version?<br>
<br>
Thanks,<br>
<br>
-------<br>
Sergei<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>