Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
fix(scripts/technical-debt-metric): avoid division by 0 (#20537)
The division by 0 affected #20521: all `ofNat` debts were removed in that PR, so one denominator became 0 giving a [CI error](https://github.com/leanprover-community/mathlib4/actions/runs/12636151506/job/35207580913). This PR fixes the issue.
- Loading branch information