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

[Andrés Sicard-Ramírez]

Hi,

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:

1. This branch is a bug-fix one (Do I need to add something else? :-))

2. We should avoid that both Agda branches (master and maintenance) diverge
too much, if possible.

3. The same reason 2, but now related to the standard library
branches.

4. We have no a scheduler for Agda releases. In any case, why delay
this bug-fix to Agda's users until the next non-bug-fix release of Agda?

Opinions?

Best,


-- 
Andrés
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda-dev/attachments/20150211/23d77c97/attachment.html