Problem fixed by check-in [89de100a2d]