[Agda-dev] Critical priority

[Andreas Abel]

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.

Cheers,
Andreas

On 16.02.2015 08:22, Ulf Norell wrote:
> Previously we've used "critical" priority to mean something that needs
> to be fixed right away because it's preventing people from using the
> affected branch. I think that's a good label to have, so I don't agree
> with marking release blockers as critical. The milestone tagging ought
> to be sufficient for identifying which issues need to be fixed before
> release.
>
> / Ulf
>
>
> _______________________________________________
> Agda-dev mailing list
> Agda-dev at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda-dev
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/