From 02c503150daef3713991d52184cc70b68e33e68e Mon Sep 17 00:00:00 2001
From: buyolitsez <buyolitsez1951@gmail.com>
Date: Tue, 23 Jun 2026 11:50:01 +0300
Subject: [PATCH] chore: auto-merge lake update PRs

---
 .github/workflows/lake-update.yml | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/.github/workflows/lake-update.yml b/.github/workflows/lake-update.yml
index 33271b968..10de5bdce 100644
--- a/.github/workflows/lake-update.yml
+++ b/.github/workflows/lake-update.yml
@@ -40,6 +40,7 @@ jobs:
         uses: leanprover-community/downstream-reports/.github/actions/bump-to-latest@main
 
       - name: Open or update PR
+        id: open-pr
         if: steps.bump.outputs.updated == 'true'
         uses: leanprover-community/downstream-reports/.github/actions/open-bump-pr@main
         with:
@@ -50,6 +51,20 @@ jobs:
           git-user-name:  mathlib-nightly-testing[bot]
           git-user-email: mathlib-nightly-testing[bot]@users.noreply.github.com
 
+      - name: Enable auto-merge for bump PR
+        if: steps.open-pr.outputs.pr-number != ''
+        env:
+          GH_TOKEN: ${{ steps.app-token.outputs.token }}
+          GH_REPO: ${{ github.repository }}
+          PR_NUMBER: ${{ steps.open-pr.outputs.pr-number }}
+        run: |
+          set -euo pipefail
+          if gh pr view "$PR_NUMBER" --json autoMergeRequest --jq '.autoMergeRequest != null' | grep -q true; then
+            echo "Auto-merge is already enabled for PR #${PR_NUMBER}."
+          else
+            gh pr merge "$PR_NUMBER" --auto
+          fi
+
   open-issue:
     runs-on: ubuntu-latest
     permissions: