Skip to content

Commit 2e5e64d

Browse files
authored
ci: use INFO=true for weekly linting (#526)
This adds back `info` messages for the weekly linting report, see leanprover-community/mathlib-ci#23 for more context.
1 parent 57e5054 commit 2e5e64d

1 file changed

Lines changed: 1 addition & 0 deletions

File tree

.github/workflows/weekly-lints.yml

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -58,6 +58,7 @@ jobs:
5858
SHA=${{ github.sha }} \
5959
REPO=${{ github.repository }} \
6060
RUN_ID=${{ github.run_id }} \
61+
INFO=true \
6162
"${CI_SCRIPTS_DIR}/reporting/zulip_build_report.sh" "${lean_outfile}" > "${GITHUB_OUTPUT}"
6263
6364
- name: Post output to Zulip

0 commit comments

Comments
 (0)