From d72370cb5be6c8f056d10dacb2cf52645becf2d2 Mon Sep 17 00:00:00 2001 From: Michael Rothgang Date: Wed, 1 Oct 2025 10:32:09 +0200 Subject: [PATCH] chore: track occurrences of 'nonrec' as technical debt Matches leanprover-community.github.io#689: only merge when that is deemed a good idea. -------- TODO: make the count more robust, for instance count all occurrences of "^nonrec " plus those of "^[private|protected] nonrec ". --- scripts/technical-debt-metrics.sh | 1 + 1 file changed, 1 insertion(+) diff --git a/scripts/technical-debt-metrics.sh b/scripts/technical-debt-metrics.sh index 216f698ad742af..401060f4183191 100755 --- a/scripts/technical-debt-metrics.sh +++ b/scripts/technical-debt-metrics.sh @@ -86,6 +86,7 @@ titlesPathsAndRegexes=( "maxHeartBeats modifications" ":^MathlibTest" "^ *set_option .*maxHeartbeats.* [0-9][0-9]*" "CommRing (Fin n) instances" "*" "^open Fin.CommRing " "NatCast (Fin n) instances" "*" "^open Fin.NatCast " + "nonrec occurrences" "*" "nonrec " ) for i in ${!titlesPathsAndRegexes[@]}; do