Skip to content

chore: migrate tests off deprecated API - #16427

Merged
TwoFX merged 1 commit into
leanprover:masterfrom
TwoFX:deprecated-tests-2
Nov 12, 2026
Merged

TwoFX merged 1 commit into
leanprover:masterfrom
TwoFX:deprecated-tests-2

Conversation

@TwoFX

@TwoFX TwoFX commented Nov 12, 2026

Copy link
Copy Markdown
Member

This PR rewrites some tests that use deprecated API to no longer trigger the deprecation linter.

This PR rewrites some tests that use deprecated API.
@TwoFX TwoFX added the changelog-no Do not include this PR in the release changelog label Nov 12, 2026
@TwoFX
TwoFX enabled auto-merge November 12, 2026 15:25
@TwoFX
TwoFX added this pull request to the merge queue Nov 12, 2026
@github-actions github-actions Bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Nov 12, 2026
Merged via the queue into leanprover:master with commit eae07dc Nov 12, 2026
22 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

changelog-no Do not include this PR in the release changelog toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant