chore: ci: do no add full-ci to lean PRs (#11369)

it triggers rebuilds and can be annoying.

scripts/lean-pr-testing-comments.sh

@@ -59,15 +59,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 full-ci"
-    # We also add the 'full-ci' label, as fixing a Mathlib breakage may require toolchains for all OSes
+    echo "Adding labels 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", "full-ci"]}'
+      -d '{"labels":["breaks-mathlib"]}'
   fi
 
   # Use GitHub API to check if a comment already exists