On Friday, 7 July 2023 at 10:39:40 UTC, Richard (Rikki) Andrew Cattermole wrote: > [snip] I didn't post this to discuss unicode characters so I would suggest people to stop derailing discussion with any of that. Thanks.