Am Sonntag, dem 08.09.2024 um 12:18 -0400 schrieb Richard Kimberly Heck: > That was my thought, as well. Simple and effective. Good, I committed to master. Note that if you cherry-pick, you both need both bfd855747ab (the indentation fix) and 0beb790a6a1945 (the actual bug fix), as the latter won't apply cleanly without the former. -- Jürgen