<div dir="auto">Hi Mietek,<div dir="auto"> Yup the plan is always to release the new version of the standard library with Agda whenever the old version is incompatible. Unfortunately I had a grant deadline yesterday so couldn't get it out immediately. Will release it in the next few hours.</div><div dir="auto">Matthew</div><div dir="auto"><br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, 17 Mar 2020, 02:53 Andrés Sicard-Ramírez, <<a href="mailto:asr@eafit.edu.co">asr@eafit.edu.co</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">On Mon, 16 Mar 2020 at 13:41, Miëtek Bak <<a href="mailto:mietek@bak.io" target="_blank" rel="noreferrer">mietek@bak.io</a>> wrote:<br>
><br>
> Can we make it a rule that the standard library gets a release at the same time as Agda?<br>
<br>
I think it isn't a good idea. Both releases procedures currently are<br>
complex and we don't need to add extra complexity. The team of<br>
standard library knew the plans for the Agda release and them we'll<br>
release a version of the standard library compatibles with Agda 2.6.1.<br>
soon.<br>
<br>
Best,<br>
<br>
<br>
-- <br>
Andrés<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank" rel="noreferrer">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote></div>