From 8eedc61a030954e3dad5a06bd750b29f54709126 Mon Sep 17 00:00:00 2001
From: Johan Commelin <johan@commelin.net>
Date: Sat, 23 Nov 2024 08:16:23 +0000
Subject: [PATCH] chore(discover-lean-pr-testing): better tracing, better
 output formatting (#19392)

---
 .github/workflows/discover-lean-pr-testing.yml | 13 ++++++++-----
 1 file changed, 8 insertions(+), 5 deletions(-)

diff --git a/.github/workflows/discover-lean-pr-testing.yml b/.github/workflows/discover-lean-pr-testing.yml
index 2bee99c8e421d..8210a3e66daab 100644
--- a/.github/workflows/discover-lean-pr-testing.yml
+++ b/.github/workflows/discover-lean-pr-testing.yml
@@ -74,9 +74,12 @@ jobs:
       run: |
         # Use the PRs from the previous step
         PRS="${{ steps.get-prs.outputs.prs }}"
+        echo "$PRS"
+        echo "===================="
         echo "$PRS" | tr ' ' '\n' > prs.txt
         MATCHING_BRANCHES=$(git branch -r | grep -f prs.txt)
         echo "$MATCHING_BRANCHES"
+        echo "===================="
 
         # Initialize an empty variable to store branches with relevant diffs
         RELEVANT_BRANCHES=""
@@ -89,25 +92,25 @@ jobs:
             # Check if the diff contains files other than the specified ones
             if echo "$DIFF_FILES" | grep -v -e 'lake-manifest.json' -e 'lakefile.lean' -e 'lean-toolchain'; then
                 # If it does, add the branch to RELEVANT_BRANCHES
-                RELEVANT_BRANCHES="$RELEVANT_BRANCHES $BRANCH"
+                RELEVANT_BRANCHES="$RELEVANT_BRANCHES\n- $BRANCH"
             fi
         done
 
         # Output the relevant branches
         echo "'$RELEVANT_BRANCHES'"
-        echo "branches=$RELEVANT_BRANCHES" >> "$GITHUB_OUTPUT"
+        printf "branches<<EOF\n%s\nEOF" "$RELEVANT_BRANCHES" >> "$GITHUB_OUTPUT"
 
     - name: Check if there are relevant branches
       id: check-branches
       run: |
         if [ -z "${{ steps.find-branches.outputs.branches }}" ]; then
-          echo "no_branches=true" >> "$GITHUB_ENV"
+          echo "branches_exist=false" >> "$GITHUB_ENV"
         else
-          echo "no_branches=false" >> "$GITHUB_ENV"
+          echo "branches_exist=true" >> "$GITHUB_ENV"
         fi
 
     - name: Send message on Zulip
-      if: env.no_branches == 'false'
+      if: env.branches_exist == 'true'
       uses: zulip/github-actions-zulip/send-message@v1
       with:
         api-key: ${{ secrets.ZULIP_API_KEY }}