> Oops, fixed in 7c380590164ea8ee40de46059d07e08a48963577, thanks!

That's a neat solution. Thanks, Ludo!