I still did not get around to implementing this. Anyone reading this and willing to come up with a pull request for it is very welcome to ping me (also privately) to get some hints on what needs to be done.
Until then: no devtoolset, please.
I still did not get around to implementing this. Anyone reading this and willing to come up with a pull request for it is very welcome to ping me (also privately) to get some hints on what needs to be done.
Until then: no devtoolset, please.