Michael Albinus <michael.albinus@gmx.de> writes:

> A bug might trigger me to do this, finally :-)

I made a bug report ;)

Cheers,
Nico