Skip to content

Commit

Permalink
chore(discover-lean-pr-testing): better tracing, better output format…
Browse files Browse the repository at this point in the history
…ting (#19392)
  • Loading branch information
jcommelin committed Nov 23, 2024
1 parent bcc3ed6 commit 8eedc61
Showing 1 changed file with 8 additions and 5 deletions.
13 changes: 8 additions & 5 deletions .github/workflows/discover-lean-pr-testing.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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=""
Expand All @@ -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 }}
Expand Down

0 comments on commit 8eedc61

Please sign in to comment.