chore: do not set release-ci label upon failed PR test (#15775)

with leanprover/lean4#5022 the need for this
should have disappeared

scripts/lean-pr-testing-comments.sh

@@ -58,14 +58,14 @@ if [[ "$branch_name" =~ ^lean-pr-testing-([0-9]+)$ ]]; then
       -H "Authorization: Bearer $TOKEN" \
       -H "X-GitHub-Api-Version: 2022-11-28" \
       https://api.github.com/repos/leanprover/lean4/issues/$pr_number/labels/builds-mathlib
-    echo "Adding labels breaks-mathlib and release-ci"
+    echo "Adding label breaks-mathlib"
     curl -L -s \
       -X POST \
       -H "Accept: application/vnd.github+json" \
       -H "Authorization: Bearer $TOKEN" \
       -H "X-GitHub-Api-Version: 2022-11-28" \
       https://api.github.com/repos/leanprover/lean4/issues/$pr_number/labels \
-      -d '{"labels":["breaks-mathlib", "release-ci"]}'
+      -d '{"labels":["breaks-mathlib"]}'
   fi
 
   # Use GitHub API to check if a comment already exists