On Oct 21, 2012 8:58 PM, "Sebastian Ramacher" <[email protected]> wrote: > Thanks for taking care of it. I guess d41f5a26e3facc929ff895e7cb41baa19875d4a > just got me confused. This commit re-adds Priority: extra.
It is possible that my co-maintainer got confused and fixed this in the wrong way. Where is this git repository you are looking at? Will check again tomorrow.

