[Agda-dev] Re: Discussion: Missing bug-fix commit in the maintenance branch

[Andrés Sicard-Ramírez]

On 11 February 2015 at 11:24, Andrés Sicard-Ramírez <asr at eafit.edu.co> wrote:
> Nils and I started a discussion about if the commit
> https://github.com/agda/agda/commit/fe37a8290b466a60d12f158c1901e4293a0e3ce9
> should or shouldn't be in the maintenance branch.
>
> Some context: The commit fixed a long-standing bug and it might break a
> number of programs (for example, the changes required in the standard
> library were
> https://github.com/agda/agda-stdlib/commit/4c8d3ae85582541f9e8778fb06b47890e483160a).
>
> I think the commit should be in the Agda maintenance branch because:

On 15 February 2015 at 04:29, Andreas Abel <abela at chalmers.se> wrote:
> Issue 1427 is also a release blocker, as well as Nisse's fix that started
> this discussion.

Since it seems Nils' commit is "experimental", I drop the discussion
of merging this commit into the maintenance branch.


-- 
Andrés