3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2026-07-14 11:15:40 +00:00

Merge pull request #6027 from YosysHQ/mmicko/skip_fix

codecov: fix not skipping when pushing on
This commit is contained in:
Miodrag Milanović 2026-07-10 16:12:03 +00:00 committed by GitHub
commit 0e82bbefe5
No known key found for this signature in database
GPG key ID: B5690EEEBB952194

View file

@ -14,7 +14,7 @@ jobs:
should_skip: ${{ steps.set_output.outputs.should_skip }} should_skip: ${{ steps.set_output.outputs.should_skip }}
steps: steps:
- id: skip_check - id: skip_check
if: ${{ github.event_name != 'merge_group' }} if: ${{ github.event_name != 'merge_group' && github.event_name != 'push' }}
uses: mmicko/skip-duplicate-actions@master uses: mmicko/skip-duplicate-actions@master
with: with:
# don't run on documentation changes # don't run on documentation changes
@ -25,7 +25,7 @@ jobs:
- id: set_output - id: set_output
run: | run: |
if [ "${{ github.event_name }}" = "merge_group" ]; then if [ "${{ github.event_name }}" = "merge_group" ] || [ "${{ github.event_name }}" = "push" ]; then
echo "should_skip=false" >> $GITHUB_OUTPUT echo "should_skip=false" >> $GITHUB_OUTPUT
else else
echo "should_skip=${{ steps.skip_check.outputs.should_skip }}" >> $GITHUB_OUTPUT echo "should_skip=${{ steps.skip_check.outputs.should_skip }}" >> $GITHUB_OUTPUT