Revert "Decrease the usage count of List.hd from 317 to 315"

This reverts commit db91ddf. Signed-off-by: Ming Lu <[email protected]>
minglumlu · Feb 27, 2024 · cfc5b63 · cfc5b63
1 parent 7741b97
commit cfc5b63
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/quality-gate.sh b/quality-gate.sh
@@ -3,7 +3,7 @@
 set -e
 
 list-hd () {
-  N=316
+  N=318
   LIST_HD=$(git grep -r --count 'List.hd' -- **/*.ml | cut -d ':' -f 2 | paste -sd+ - | bc)
   if [ "$LIST_HD" -eq "$N" ]; then
     echo "OK counted $LIST_HD List.hd usages"