Processed: Re: java.lang.ClassCastException: java.io.File cannot be cast to java.lang.Class

[Debian Bug Tracking System]

Processing control commands:

> severity -1 grave
Bug #798699 [freecol] java.lang.ClassCastException: java.io.File cannot be cast to java.lang.Class
Ignoring request to change severity of Bug 798699 to the same value.
> tags -1 stretch sid
Bug #798699 [freecol] java.lang.ClassCastException: java.io.File cannot be cast to java.lang.Class
Ignoring request to alter tags of bug #798699 to the same tags previously set

-- 
798699: http://bugs.debian.org/cgi-bin/bugreport.cgi?bug=798699
Debian Bug Tracking System
Contact owner at bugs.debian.org with problems