chore: update lean-pr-testing reporting logic, now that the linter al…

…ways runs (#12202) As reported [elsewhere](leanprover/lean4#3808 (comment)). Co-authored-by: Scott Morrison <[email protected]>
leanprover-community · Apr 18, 2024 · 071b2ee · 071b2ee
1 parent a4c2a1e
commit 071b2ee
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/scripts/lean-pr-testing-comments.sh b/scripts/lean-pr-testing-comments.sh
@@ -83,6 +83,8 @@ if [[ "$branch_name" =~ ^lean-pr-testing-([0-9]+)$ ]]; then
     message="- 🟡 Mathlib branch $branch build against this PR was cancelled. ($current_time) [View Log]($WORKFLOW_URL)"
   elif [ "$CHECK_OUTCOME" == "success" ]; then
     message="- ✅ Mathlib branch $branch has successfully built against this PR. ($current_time) [View Log]($WORKFLOW_URL)"
+  elif [ "$BUILD_OUTCOME" == "failure" ] ; then
+    message="- 💥 Mathlib branch $branch build failed against this PR. ($current_time) [View Log]($WORKFLOW_URL)"
   elif [ "$CHECK_OUTCOME" == "failure" ]; then
     message="- ❌ Mathlib branch $branch built against this PR, but lean4checker failed. ($current_time) [View Log]($WORKFLOW_URL)"
   elif [ "$LINT_OUTCOME" == "failure" ]; then
@@ -95,8 +97,6 @@ if [[ "$branch_name" =~ ^lean-pr-testing-([0-9]+)$ ]]; then
     message="- ❌ Mathlib branch $branch built against this PR, but was unexpectedly noisy. ($current_time) [View Log]($WORKFLOW_URL)"
   elif [ "$TEST_OUTCOME" == "failure" ]; then
     message="- ❌ Mathlib branch $branch built against this PR, but testing failed. ($current_time) [View Log]($WORKFLOW_URL)"
-  elif [ "$BUILD_OUTCOME" == "failure" ] ; then
-    message="- 💥 Mathlib branch $branch build failed against this PR. ($current_time) [View Log]($WORKFLOW_URL)"
   else
     message="- 🟡 Mathlib branch $branch build this PR didn't complete normally. ($current_time) [View Log]($WORKFLOW_URL)"
   fi