… 16 months later I have finally managed to leave a comment on the appropriate ticket. Seems like my inexperienced earlier self had given up after realizing that the ticket was already existing
So just for completeness, here is the link to the ticket:
6 Likes