diff --git a/.github/workflows/autograding.yml b/.github/workflows/autograding.yml index db8e820e..307d71a3 100644 --- a/.github/workflows/autograding.yml +++ b/.github/workflows/autograding.yml @@ -26,7 +26,7 @@ jobs: env: BROWSER: chrome-container run: mvn -V --color always -ntp clean verify --file pom.xml '-Djenkins.test.timeout=5000' '-Dgpg.skip' -Ppit | tee maven.log - - name: Extract pull request number + - name: 'Extract pull request number' uses: jwalton/gh-find-current-pr@v1 id: pr - name: Run Autograding diff --git a/.github/workflows/reporting.yml b/.github/workflows/reporting.yml index e3b40ad7..ea0ed742 100644 --- a/.github/workflows/reporting.yml +++ b/.github/workflows/reporting.yml @@ -150,14 +150,14 @@ jobs: status: ${{ steps.metrics.outputs.warnings }} color: 'orange' path: badges/warnings.svg - - name: Commit badge + - name: Commit updated badges continue-on-error: true run: | git config --local user.email "action@github.com" git config --local user.name "GitHub Action" git add badges/*.svg git commit -m "Update badges with results from latest autograding" - - name: Push badge commit + - name: Push updated badges to GitHub repository uses: ad-m/github-push-action@master if: ${{ success() }} with: