On Tue 11 Dec 2018 at 13:21:45 +0000, Brian Potkin wrote: [...]
> A bug report is in order, I think. https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=916267 I may as well throw in https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=911844 https://bugs.debian.org/cgi-bin/bugreport.cgi?bug=911702 as well. Regards, Brian.
