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

What a lovely Christmas present ;)

/Mathias