minor change

Co-authored-by: Weijia Wang <9713184+wegank@users.noreply.github.com>
This commit is contained in:
Tobias Bora 2023-01-08 12:06:50 +01:00 committed by Manuel Bärenz
parent 92cbb32090
commit 517c661748