Commit 2025-12-11 19:40 2f7cf63b

fix(ci): use bot token for discover-lean-pr-testing merges (#32722) This PR fixes an issue where merge commits from lean-pr-testing-NNNN branches weren't triggering CI. The discover-lean-pr-testing.yml workflow was using the default GITHUB_TOKEN and github-actions identity when pushing merge commits. Due to GitHub's "actions don't trigger actions" policy, these commits didn't trigger CI runs. This aligns with how nightly_bump_toolchain.yml and nightly_merge_master.yml handle pushes - using the NIGHTLY_TESTING token and the leanprover-community-mathlib4-bot identity. Discovered via https://leanprover.zulipchat.com/#narrow/channel/428973-nightly-testing/topic/Mathlib.20status.20updates/near/563147856 🤖 Prepared with Claude Code