update leaderboard #18

	name: Publish Leaderboard

	on:
	push:
	branches: [ main ]
	paths:
	- "leaderboard/leaderboard.csv"

	jobs:
	render:
	runs-on: ubuntu-latest
	steps:
	- uses: actions/checkout@v4

	- name: Set up Python
	uses: actions/setup-python@v5
	with:
	python-version: "3.10"

	- name: Install dependencies
	run: pip install pandas

	- name: Render leaderboard markdown
	run: python competition/render_leaderboard.py

	- name: Sync leaderboard to docs
	run: cp leaderboard/leaderboard.csv docs/leaderboard.csv

	- name: Commit rendered leaderboard
	run: \|
	if git diff --quiet; then
	echo "No changes."
	exit 0
	fi
	git config user.name "github-actions"
	git config user.email "github-actions@users.noreply.github.com"
	git add leaderboard/leaderboard.md docs/leaderboard.csv
	git commit -m "Update leaderboard"
	git push

Provide feedback