Skip to content

chore: auto-merge lake update PRs#676

Open
buyolitsez wants to merge 1 commit into
leanprover:mainfrom
buyolitsez:294
Open

chore: auto-merge lake update PRs#676
buyolitsez wants to merge 1 commit into
leanprover:mainfrom
buyolitsez:294

Conversation

@buyolitsez

@buyolitsez buyolitsez commented Jun 23, 2026

Copy link
Copy Markdown

Closes #294

  • Capture the PR number produced by downstream-reports/open-bump-pr
  • Auto-merge for the automated lake update bump PR
  • Skip re-enabling auto-merge when it is already requested

This PR was prepared with Codex (gpt 5.5, xhigh)

@chenson2018, could you please review it?

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Automate lake update PRs

1 participant