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 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 EIVE/-/pipeline/pr-main This commit looks good Details	2023-10-27 14:26:16 +02:00
Robin Müller	b08f9d9af6	more cleaning EIVE/-/pipeline/head This commit looks good Details	2023-10-27 12:28:55 +02:00