Am Mittwoch, dem 09.08.2023 um 14:51 +0200 schrieb Pavel Sanda: > I agree, this looks like copy-paste error, going back to 1efef55; > thought it might be good to get Juergen's nod. Probably cut and paste error, right. -- Jürgen