Skip to content

leaderboard: fix bugs #3

leaderboard: fix bugs

leaderboard: fix bugs #3

Workflow file for this run

name: Leaderboard
on:
push:
branches: [ "main" ]
workflow_dispatch: {}
jobs:
build:
runs-on: ubuntu-latest
permissions:
contents: write
steps:
- uses: actions/checkout@v4
- name: Update Leaderboard in README.md
run: ./leaderboard-replace.sh
- name: Output README.md changes for debugging
run: git diff README.md
- name: Commit and Push changes
run: |
set -e
if ! git diff --no-patch --exit-code README.md; then
git config --global user.name "${GITHUB_ACTOR}"
git config --global user.email "${GITHUB_ACTOR}@users.noreply.github.com"
git commit -am "README.md: update leaderboard" \
git push
else
echo "README.md unchanged, not committing"
fi