File tree Expand file tree Collapse file tree 1 file changed +1
-1
lines changed
Expand file tree Collapse file tree 1 file changed +1
-1
lines changed Original file line number Diff line number Diff line change 4646 test-outcome : ${{ steps.test.outcome }}
4747 defaults : # On Hoskinson runners, landrun is already installed.
4848 run : # note that .pr-branch/.lake must be created in a step below before we use this
49- shell : landrun --rox /usr --ro /etc/timezone --rw /dev --rox /home/lean/.elan --rox /home/lean/actions-runner/_work --rox /home/lean/.cache/mathlib/ --rw pr-branch/.lake/ --rw cache-staging/ -- env PATH --env HOME --env GITHUB_OUTPUT --env CI -- bash -euxo pipefail {0}
49+ shell : landrun --rox /usr --ro /etc/timezone --rw /dev --rox /home/lean/.elan --rox /home/lean/actions-runner/_work --rox /home/lean/.cache/mathlib/ --rw pr-branch/.lake/ --env PATH --env HOME --env GITHUB_OUTPUT --env CI -- bash -euxo pipefail {0}
5050 steps :
5151 - name : job info
5252 env :
You can’t perform that action at this time.
0 commit comments