more cleaning #252

Merged

meggert merged 3 commits from str-cleaning into main

2023-10-27 14:37:00 +02:00

Author	SHA1	Message	Date
Marius Eggert	76e80c259c	Merge branch 'main' into str-cleaning Some checks are pending EIVE/-/pipeline/pr-main Build queued... Details	2023-10-27 14:36:50 +02:00
Robin Müller	18728731ed	Merge branch 'main' into str-cleaning All checks were successful EIVE/-/pipeline/pr-main This commit looks good Details	2023-10-27 14:26:16 +02:00
Robin Mueller	b08f9d9af6	more cleaning All checks were successful EIVE/-/pipeline/head This commit looks good Details	2023-10-27 12:28:55 +02:00