Skip to content

Commit 51fb57f

Browse files
committed
fix(ci): use bot token for discover-lean-pr-testing merges
Use the NIGHTLY_TESTING token and bot identity when pushing merge commits from lean-pr-testing branches. Previously, these commits were pushed with the default GITHUB_TOKEN and github-actions identity, which meant they didn't trigger CI due to GitHub's "actions don't trigger actions" policy. This aligns with how nightly_bump_toolchain.yml and nightly_merge_master.yml handle pushes. 🤖 Prepared with Claude Code
1 parent ee135c1 commit 51fb57f

1 file changed

Lines changed: 3 additions & 2 deletions

File tree

.github/workflows/discover-lean-pr-testing.yml

Lines changed: 3 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -18,11 +18,12 @@ jobs:
1818
with:
1919
ref: nightly-testing
2020
fetch-depth: 0 # Fetch all branches
21+
token: ${{ secrets.NIGHTLY_TESTING }}
2122

2223
- name: Set up Git
2324
run: |
24-
git config --global user.name "github-actions"
25-
git config --global user.email "github-actions@github.com"
25+
git config --global user.name "leanprover-community-mathlib4-bot"
26+
git config --global user.email "leanprover-community-mathlib4-bot@users.noreply.github.com"
2627
2728
- name: Configure Lean
2829
uses: leanprover/lean-action@434f25c2f80ded67bba02502ad3a86f25db50709 # v1.3.0

0 commit comments

Comments
 (0)