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

[Nils Anders Danielsson]

On 2015-02-11 17:24, Andrés Sicard-Ramírez wrote:
> 1. This branch is a bug-fix one (Do I need to add something else? :-))

The "bug" was introduced—on purpose—to fix a performance issue in the
original mixfix parser, only a couple of days after mixfix operator
parsing was implemented. No version of Agda 2 has ever been released
without this bug. I don't know if anyone besides me and Ulf were aware
of the issue. However, my bug fix does break programs.

Perhaps I shouldn't have used the term "bug" in my commit message. Would
you be willing to drop this discussion if we called it a "modification
of the operator grammar" instead?

-- 
/NAD