Closed RealCLanger closed 4 months ago
clean cherry-pick from commit 1106762a444e97830a99f025e650dea919e4aa8b
fixes #1714
Hello @RealCLanger, this pull request fulfills all formal requirements.
clean cherry-pick from commit 1106762a444e97830a99f025e650dea919e4aa8b
fixes #1714