@sgiehl opened this Pull Request on December 11th 2021 Member


fixes #18481


@sgiehl commented on December 13th 2021 Member

Only wanted to change as less as possible, as it is actually a third party library. Even though we should try to get rid of it some day.

This Pull Request was closed on December 14th 2021
Powered by GitHub Issue Mirror