File tree Expand file tree Collapse file tree 1 file changed +2
-2
lines changed
Expand file tree Collapse file tree 1 file changed +2
-2
lines changed Original file line number Diff line number Diff line change @@ -331,7 +331,7 @@ jobs:
331331 - name : begin gh-problem-match-wrap for build step
332332 uses : leanprover-community/gh-problem-matcher-wrap@20007cb926a46aa324653a387363b52f07709845 # 2025-04-23
333333 with :
334- action : add # In order to be able to run a multiline script, we need to add/remove the problem matcher before and after.
334+ action : add # In order to be able to run a multiline script, we need to add/remove the problem matcher before and after.t
335335 linters : lean
336336 - name : build mathlib
337337 id : build
@@ -424,7 +424,7 @@ jobs:
424424 if : ${{ steps.build.outcome == 'success' }}
425425 shell : bash
426426 run : |
427- if find cache-staging -type f -name '*.ltar' -print -quit | grep -q .;
427+ if find cache-staging -type f -name '*.ltar' -print -quit | grep -q .; then
428428 echo "has_files=true" >> "$GITHUB_OUTPUT"
429429 else
430430 echo "has_files=false" >> "$GITHUB_OUTPUT"
You can’t perform that action at this time.
0 commit comments