Skip to content

Bump mathlib dependency to 1f8806b - #206

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

RemyDegenne merged 1 commit into
mainfrom
hopscotch/lkg-bump

Conversation

@github-actions

@github-actions github-actions Bot commented Jul 31, 2026 •

Copy link
Copy Markdown
Contributor

Bump mathlib dependency to 1f8806b: fix: adaptations for batteries #1927 (#42229) (2026-07-31)
Previously at: 2705f82: chore(Util/CountHeartbeats): deprecate the global #count_heartbeats command (#42274) (2026-07-30)


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-08-01 by this workflow run. It is an automated bump using downstream-reports/open-bump-pr.

@github-actions
github-actions Bot force-pushed the hopscotch/lkg-bump branch from 14190ee to 73efe39 Compare August 1, 2026 06:55
@github-actions github-actions Bot changed the title Bump mathlib dependency to ce88332 Bump mathlib dependency to 1f8806b Aug 1, 2026
@RemyDegenne
RemyDegenne merged commit e25bc05 into main Aug 1, 2026
1 check passed
@RemyDegenne
RemyDegenne deleted the hopscotch/lkg-bump branch August 1, 2026 10:16
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