Just for the record, I've filed a Debian bug report as ticket #723903, see here: http://bugs.debian.org/cgi-bin/bugreport.cgi?bug=723903
Just for the record, I've filed a Debian bug report as ticket #723903, see here: http:// bugs.debian. org/cgi- bin/bugreport. cgi?bug= 723903