On Thursday, 17 October 2019 at 20:56:54 UTC, Dennis wrote: > I was surprised by him mentioning that as well. I'm glad it > stayed too, since I actually use them. Indeed, me too. And they are definitely still there and I'd be quite sad if they disappeared.