Merge pull request #5844 from psafont/qgate

Author: psafont

quality-gate.sh

@@ -3,7 +3,7 @@
 set -e
 
 list-hd () {
-  N=304
+  N=302
   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"