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
Severity set to 'grave' from 'important'
> tags -1 stretch sid
Bug #798699 [freecol] java.lang.ClassCastException: java.io.File cannot be cast to java.lang.Class
Added tag(s) sid and stretch.

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