On Tue, 19 Jan 2021, Gerald Pfeifer wrote: > Log: > Revert r562049 which I committed by mistake. > > Pointy hat: gerald I *always* do a diff with otherwise exactly the same command line before committing. Except this time. :-( Sorry about that. Gerald