ci: add tech debt label#40601
Conversation
PR summary 1049e60a54Import changes for modified filesNo significant changes to the import graph Import changes for all files
|
Restore Mathlib/Analysis/Normed/Group/Basic.lean and scripts/nolints_prime_decls.txt to their master state, keeping only the CI workflow change on this branch. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
|
Presumably I can't actually test that this works because security dictates that the PR summary workflow label control should only act on maintainer approved changes. Nevertheless, it seems to me like it should work. |
This PR adds a step to the PR summary bot to make it add the "tech debt" label to PRs that decrease tech debt.
This PR was made with the assistance of Claude code
Thanks to Felix for this idea. Zulip discussion here #mathlib4 > Technical Debt Counters @ 💬