Merge forgotten changes from new-frontend #2

Merged
mdivecky merged 2 commits from new-frontend into main 2023-08-17 12:26:16 +02:00

2 commits