The bug no longer occurs. It disappeared after an apt-get update (NOT yet followed by an upgrade)! Don't know why; anyway, it can now be marked "resolved" (or sent to /dev/null). Regards, Jan