From cfc5b6334ce140850626829a3baac0d3fb510de1 Mon Sep 17 00:00:00 2001
From: Ming Lu <ming.lu@cloud.com>
Date: Tue, 27 Feb 2024 19:14:20 +0800
Subject: [PATCH] Revert "Decrease the usage count of List.hd from 317 to 315"

This reverts commit db91ddf593d7b0b368535874ef45605492d04e8c.

Signed-off-by: Ming Lu <ming.lu@cloud.com>
---
 quality-gate.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/quality-gate.sh b/quality-gate.sh
index d33edacff02..224e852aa32 100755
--- 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"