Skip to content
Open
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 4 additions & 0 deletions .github/workflows/develop.yml
Original file line number Diff line number Diff line change
Expand Up @@ -18,6 +18,10 @@ permissions:
contents: read # to fetch code (actions/checkout)
checks: write # to create new checks (coverallsapp/github-action)

concurrency:
group: ${{ github.workflow }}-${{ github.ref }}
cancel-in-progress: true

Comment on lines +21 to +24

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Here's a Gemini Pro review, does this make sense?

A Minor Optimization to Consider (The github.ref Gotcha)

The code you provided uses this group logic:

concurrency:
  group: ${{ github.workflow }}-${{ github.ref }}
  cancel-in-progress: true

This will work fine, but there is a slight quirk with how GitHub Actions handles github.ref:

  • When a workflow is triggered by a push, github.ref evaluates to something like refs/heads/feature-branch.
  • When triggered by a pull_request, github.ref evaluates to a system ref like refs/pull/123/merge.

Because these refs are different, if a contributor pushes a new commit to a branch that currently has a PR open, GitHub Actions actually fires two workflows in two different concurrency groups.

GitHub's widely recommended best practice to group these together seamlessly is to use github.head_ref || github.ref:

concurrency:
  group: ${{ github.workflow }}-${{ github.head_ref || github.ref }}
  cancel-in-progress: true

Why this is better:
github.head_ref is only available during pull_request events and contains the actual branch name (e.g., feature-branch). If it's a standard push event, it falls back to github.ref. This ensures that PR updates and direct branch pushes are grouped together much more cleanly, reducing the chance of edge-case race conditions where a PR build and a push build try to run at the same time.

Combined with your stop-build script, either method will successfully save you CI time, but the github.head_ref addition is the standard way to make it bulletproof.

Copy link
Copy Markdown
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

We have previously decided that push trigger and pull request trigger are separated and should run independently.
By default, we have already made it so if one has a PR open for a given branch, the CI will not run. This allows contributor that matures the work in branches before submitting a PR to still get the automation to work.

Now, Gemini suggestion wouldn't work anyway because the concurrency group is specific to the repo. In other term, the PR one would be as mixxxdj/mixxx:${{ github.workflow }}-${{ github.ref }}, and the branch push would be ronso0/mixxx:${{ github.workflow }}-${{ github.ref }}, so both wouldn't cancel each other

Copy link
Copy Markdown
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Okay, thanks for the explanation (though must admit that I'm not into it to fully understand everything).

jobs:
stop-build:
name: Check if build should be stopped
Expand Down
Loading