Publish leaderboard through gh-pages #2

	name: Publish leaderboard branch

	"on":
	push:
	branches:
	- main
	paths:
	- "leaderboard/**"
	- ".github/workflows/leaderboard-pages.yml"
	workflow_dispatch:

	permissions:
	contents: write

	jobs:
	publish:
	runs-on: ubuntu-latest
	steps:
	- name: Checkout
	uses: actions/checkout@v4
	with:
	fetch-depth: 0

	- name: Publish leaderboard to gh-pages
	shell: bash
	run: \|
	set -euo pipefail
	git config user.name "github-actions[bot]"
	git config user.email "41898282+github-actions[bot]@users.noreply.github.com"

	git fetch origin gh-pages --depth=1 \|\| true
	rm -rf /tmp/twinrouterbench-pages

	if git rev-parse --verify origin/gh-pages >/dev/null 2>&1; then
	git worktree add /tmp/twinrouterbench-pages origin/gh-pages
	else
	git worktree add --detach /tmp/twinrouterbench-pages
	git -C /tmp/twinrouterbench-pages rm -r . >/dev/null 2>&1 \|\| true
	fi

	rsync -a --delete --exclude ".git" leaderboard/ /tmp/twinrouterbench-pages/
	cd /tmp/twinrouterbench-pages
	git add -A

	if git diff --cached --quiet; then
	echo "No leaderboard changes to publish."
	exit 0
	fi

	git commit -m "Deploy leaderboard"
	git push origin HEAD:gh-pages

Provide feedback