Michael Albinus <michael.albinus@gmx.de> writes: >>From my pov, we could close the bug, unless the problem happens again. > >> Paul OK; closing this bug report, then.