Skip to content

[Merged by Bors] - chore: don't disable deprecation warnings#24001

Closed
eric-wieser wants to merge 1 commit intomasterfrom
eric-wieser-patch-2
Closed

[Merged by Bors] - chore: don't disable deprecation warnings#24001
eric-wieser wants to merge 1 commit intomasterfrom
eric-wieser-patch-2

Conversation

@eric-wieser
Copy link
Copy Markdown
Member


Open in Gitpod

@eric-wieser eric-wieser added the easy < 20s of review time. See the lifecycle page for guidelines. label Apr 13, 2025
@github-actions
Copy link
Copy Markdown

PR summary 162246d481

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.


Decrease in tech debt: (relative, absolute) = (1.00, 0.01)
Current number Change Type
96 -1 disabled deprecation lints

Current commit 162246d481
Reference commit ff99cdaecc

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@github-actions github-actions bot added the t-analysis Analysis (normed *, calculus) label Apr 13, 2025
@j-loreaux
Copy link
Copy Markdown
Contributor

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label Apr 13, 2025
mathlib-bors bot pushed a commit that referenced this pull request Apr 13, 2025
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Apr 13, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: don't disable deprecation warnings [Merged by Bors] - chore: don't disable deprecation warnings Apr 13, 2025
@mathlib-bors mathlib-bors bot closed this Apr 13, 2025
@mathlib-bors mathlib-bors bot deleted the eric-wieser-patch-2 branch April 13, 2025 16:02
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

easy < 20s of review time. See the lifecycle page for guidelines. ready-to-merge This PR has been sent to bors. t-analysis Analysis (normed *, calculus)

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants