[Agda-dev] Critical priority

[Andrés Sicard-Ramírez]

On 16 February 2015 at 02:27, Andreas Abel <abela at chalmers.se> wrote:
> I agree that "critical" should be reserved to emergencies (like compilation
> failure).
>
> However, the "high" priority is seeing some inflation, so I think we should
> add "Priority-Highest" to separate out the most important things with high
> prio.

I agree. I miss a Priority-Highest label when I labelled the release
blockers issues as Priority-Critical. I'll fix this in the bug
tracker.

Best,

-- 
Andrés