Skip to content

Commit

Permalink
fix: make CI-task "check for noisy stdout lines" more verbose. (#7868)
Browse files Browse the repository at this point in the history
linter warnings print the following messages to stdout:

```
stdout:
./././MyProject/MyFile.lean:19:53: warning: unused variable `x` [linter.unusedVariables]
./././MyProject/MyFile.lean:19:53: warning: unused variable `y` [linter.unusedVariables]
```

With this change, the CI would at least print the first line after `stdout:`, partially helping with debugging.
  • Loading branch information
joneugster committed Nov 1, 2023
1 parent 62ca97d commit 8f16322
Show file tree
Hide file tree
Showing 4 changed files with 4 additions and 4 deletions.
2 changes: 1 addition & 1 deletion .github/workflows/bors.yml
Original file line number Diff line number Diff line change
Expand Up @@ -179,7 +179,7 @@ jobs:
- name: check for noisy stdout lines
run: |
! grep "stdout:" stdout.log
! grep --after-context=1 "stdout:" stdout.log
- name: build library_search cache
run: lake build -KCI MathlibExtras
Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/build.yml
Original file line number Diff line number Diff line change
Expand Up @@ -185,7 +185,7 @@ jobs:
- name: check for noisy stdout lines
run: |
! grep "stdout:" stdout.log
! grep --after-context=1 "stdout:" stdout.log
- name: build library_search cache
run: lake build -KCI MathlibExtras
Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/build.yml.in
Original file line number Diff line number Diff line change
Expand Up @@ -165,7 +165,7 @@ jobs:

- name: check for noisy stdout lines
run: |
! grep "stdout:" stdout.log
! grep --after-context=1 "stdout:" stdout.log

- name: build library_search cache
run: lake build -KCI MathlibExtras
Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/build_fork.yml
Original file line number Diff line number Diff line change
Expand Up @@ -183,7 +183,7 @@ jobs:
- name: check for noisy stdout lines
run: |
! grep "stdout:" stdout.log
! grep --after-context=1 "stdout:" stdout.log
- name: build library_search cache
run: lake build -KCI MathlibExtras
Expand Down

0 comments on commit 8f16322

Please sign in to comment.