diff --git a/scripts/lean-pr-testing-comments.sh b/scripts/lean-pr-testing-comments.sh index df6bcb257f4fb..189a6ea6ac536 100755 --- a/scripts/lean-pr-testing-comments.sh +++ b/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