Magnus Norddahl a4fae58685 Rename action workflow as github doesn't group them and two workflows with the same name is annoying		2023-12-31 07:31:04 +01:00
..
workflows	Rename action workflow as github doesn't group them and two workflows with the same name is annoying	2023-12-31 07:31:04 +01:00