> > https://debbugs.gnu.org/cgi/bugreport.cgi?bug=13193 > > Thanks for the tip. I hadn't thought to look in the Debian bug > tracker. FYI, it is on GNU's BTS, not Debian. debbugs is not used for only Debian. -- Kazuhiro Ito