![](https://secure.gravatar.com/avatar/498dccbac38d2bd682334bb6b6baaa27.jpg?s=120&d=mm&r=g)
2 Feb
2024
2 Feb
'24
3:16 a.m.
I have stumbeld across the same bug. Seems to be very elementary, but is still present after many years. Sigh.