Skip to content

Bump mathlib dependency to 045acef - #260

Merged
RemyDegenne merged 1 commit into
mainfrom
hopscotch/lkg-bump
Sep 24, 2026
Merged

RemyDegenne merged 1 commit into
mainfrom
hopscotch/lkg-bump

Conversation

@github-actions

@github-actions github-actions Bot commented Sep 23, 2026 •

Copy link
Copy Markdown
Contributor

Bump mathlib dependency to 045acef: feat(cache): record transport fields on a failed transfer (#44048) (2026-09-23)
Previously at: a379806: refactor(CategoryTheory): insert missing Functor.op compatibility isomorphisms (#43567) (2026-09-22)


This is an automated dependency bump to the latest commit this project is known to build against (its last-known-good commit). lake build was run against the new commit before this PR was opened and succeeded, so it should be mergeable as-is.

Only lake build is checked, though — if your own CI does more (linting, failing on warnings, downstream tests, …), run it on this PR before merging.

Warning

This PR was opened by the default github-actions[bot] identity, so your repository's own CI does not run until a maintainer approves it — GitHub holds the workflow runs (push / pull_request) on PRs opened under the built-in GITHUB_TOKEN until a user with write access approves them.

Use the Approve and run workflows button on this PR to run your CI. To run it automatically on every automated bump PR (no per-PR approval), open them under a GitHub App token instead: see the authentication guide.

This PR was last updated on 2026-09-24 by this workflow run. It is an automated bump using downstream-reports/open-bump-pr.

@github-actions github-actions Bot changed the title Bump mathlib dependency to 2f3d8f6 Bump mathlib dependency to 95c90ee Sep 23, 2026
@github-actions github-actions Bot changed the title Bump mathlib dependency to 95c90ee Bump mathlib dependency to 045acef Sep 24, 2026
@RemyDegenne
RemyDegenne merged commit c3e2b29 into main Sep 24, 2026
1 check passed
@RemyDegenne
RemyDegenne deleted the hopscotch/lkg-bump branch September 24, 2026 09:05
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.

1 participant