Skip to content

fix: Updated duplicated GitHub workflow name (#550) #1190

fix: Updated duplicated GitHub workflow name (#550)

fix: Updated duplicated GitHub workflow name (#550) #1190

Workflow file for this run

name: Test OnDemand Loop
on:
workflow_dispatch:
pull_request:
push:
branches: [ main ]
jobs:
build-and-test-ood-loop:
name: Run tests
runs-on: ubuntu-latest
steps:
- name: Checkout ${{ github.sha }}
uses: actions/checkout@v6
- name: Run tests
run: make test
coverage-and-badges:
name: Coverage & badges (main only)
needs: build-and-test-ood-loop
runs-on: ubuntu-latest
if: github.event_name == 'push' && github.ref == 'refs/heads/main'
permissions:
contents: write
steps:
- name: Generate GitHub App token
id: app-token
uses: actions/create-github-app-token@v2
with:
app-id: ${{ secrets.APP_ID }}
private-key: ${{ secrets.APP_PRIVATE_KEY }}
- name: Checkout ${{ github.sha }}
uses: actions/checkout@v6
with:
token: ${{ steps.app-token.outputs.token }}
- name: Generate coverage & badges
run: make coverage
- name: Print coverage summary to GitHub Actions UI
run: cat docs/badges/coverage-summary.txt
- name: Git setup
run: |
git config --global user.name "github-actions"
git config --global user.email "[email protected]"
- name: Commit and push badges
run: |
git add docs/badges
git commit -m "Update coverage badges [skip ci]" || echo "No changes"
git push origin main