On Thu, Aug 10, 2023 at 02:00:20PM +0200, Jürgen Spitzmüller wrote: > 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. Fix committed. Pavel