> Done. Bug 16219 created. > http://debbugs.gnu.org/cgi/bugreport.cgi?bug=16219 Oh well, I fixed it a few days ago already ;-)