Give Github Actions sane names so they can be selected as required#571

Merged

Lohrer merged 1 commit intodevelopfrom actions

Dec 20, 2023

+4-2

Commits on Dec 19, 2023

Give Github Actions sane names so they can be selected as required
Lohrer
committed