Commits on Oct 17, 2023

1. 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.
   
   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.

   

   dvdhrm committed Oct 17, 2023
   Configuration menu

   • View commit details
   • Copy full SHA for cdc7c1b
   • Browse repository at this point

   Copy the full SHA

   cdc7c1b View commit details

   Browse the repository at this point in the history