Vadim Zeitlin 8505c48a34 Cancel in progress builds of PRs when a new one starts ... Add a snippet based on the example in https://docs.github.com/en/actions/using-jobs/using-concurrency#example-only-cancel-in-progress-jobs-or-runs-for-the-current-workflow to all CI workflows to cancel the currently running build when a new one starts. This should ensure that we don't keep building the old version of the PR after a new one has been pushed.		2023-02-21 14:58:57 +01:00
..
ISSUE_TEMPLATE	Refactor issue templates using HTML comments	2022-09-27 23:27:42 +02:00
workflows	Cancel in progress builds of PRs when a new one starts	2023-02-21 14:58:57 +01:00
CONTRIBUTING.md	Revert "Explain that GitHub PRs are temporarily disabled"	2022-01-12 23:42:18 +01:00