Skip to content

Commit

Permalink
chore: simplify lean4checker reporting
Browse files Browse the repository at this point in the history
  • Loading branch information
kim-em committed Oct 14, 2024
1 parent d990505 commit cb31cbf
Showing 1 changed file with 1 addition and 8 deletions.
9 changes: 1 addition & 8 deletions .github/workflows/lean4checker.yml
Original file line number Diff line number Diff line change
Expand Up @@ -79,13 +79,6 @@ jobs:
cd ..
lake env lean4checker/.lake/build/bin/lean4checker
- id: ci_url
run: |
url=https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}
curl -s "${url}" |
# extract the CI run number from the unique line that matches ` href=".../job/[job number]"`
awk -v url="${url}" -F'/' '/^ *href/ {gsub(/"/, "", $NF); printf("summary<<EOF\n%s/job/%s\nEOF", url, $NF)}' >> "$GITHUB_OUTPUT"
- name: Post success message on Zulip
if: success()
uses: zulip/github-actions-zulip/send-message@v1
Expand All @@ -97,7 +90,7 @@ jobs:
type: 'stream'
topic: 'lean4checker'
content: |
✅ lean4checker [succeeded](${{ steps.ci_url.outputs.summary }}) on ${{ github.sha }}
✅ lean4checker [succeeded](https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}) on ${{ github.sha }}
- name: Post failure message on Zulip
if: failure()
Expand Down

0 comments on commit cb31cbf

Please sign in to comment.