> > > That, to me, is much clearer than the "_int" suffix. > > > > This sounds like an excellent idea to me. > > "Someone" should create a PR...
I wouldn't mind doing it alongside the other changes in #9274, but I'd prefer my alternative proposal, which I just posted before. That is, if you agree of course. If you insist on doing it as a separate PR, I don't mind. But it does not make sense to start on it before #9274 has been accepted and merged. Matthias
