Auto merge of #12835 - dvdhrm:pr/contrib-concurrency, r=weihanglo

ci/contrib: use separate concurrency group

Run the contrib workflow in its own concurrency group to avoid multiple runs causing conflicting git pushes.

The contrib workflow pushes to the gh-pages branch, and thus is not safe to be run multiple times in parallel. Given that github-actions can stall workflow runs for quite some time, multiple executions can overtake each other. By using concurrency groups, all workflow runs will wait until previous runs completed.

Given that the workflow uses orphan-branches and forced pushes, conflicting workflows will not fail, but might produce outdated data if they overtake each other.

We explicitly disable cancellation to get better diagnostics and more easily find the first possible run that failed. Since these workflow runs are rather fast, and only run on master, cancellation seems not necessary.

Author: bors

.github/workflows/contrib.yml

@@ -4,6 +4,10 @@ on:
     branches:
       - master
 
+concurrency:
+  cancel-in-progress: false
+  group: "gh-pages"
+
 permissions:
   contents: read