5 Commits

Author	SHA1	Message	Date
Alexander A. Klimov	0fe13051b7	GHA: cancel runs on PR, but not on push ... In a PR one top commit replaces the previous one. But the central branches are more like timelines. It's nice to have red crosses in a such timeline as clear indicators that something was actually broken.	2023-11-17 15:54:03 +01:00
Johannes Meyer	9f757dd551	Run only a single job per workflow matrix at a time ... This limits each run of these workflows to a single active matrix job. This means, for each PR, merge or release only five jobs run concurrently.	2023-01-20 15:44:40 +01:00
Alexander A. Klimov	1d8cffe9b9	GHA: let GitHub cancel redundant jobs ... This will also cancel not yet finished master builds, but that's not too bad.	2023-01-19 10:47:14 +01:00
Julian Brost	4c4731a461	GitHub Actions: pin Windows Server version to 2019	2022-02-04 14:09:52 +01:00
Alexander A. Klimov	0e038a0916	Split GitHub actions ... ... to allow to re-run a minimum.	2021-07-26 17:38:33 +02:00