This repository has been archived by the owner on Jul 24, 2024. It is now read-only.
Merge remote-tracking branch 'origin/master' into eric-wieser/exp-rat #121021
eric-wieserbuild.yml
on: push
Build mathlib
15m 1s
Lint style
34s
Cancel Previous Runs (CI)
2s
Post-CI job
0s
Annotations
7 errors and 1 warning
|
Lint style:
src/analysis/normed_space/exponential.lean#L304
ERR_LIN: Line has more than 100 characters
|
|
Lint style:
src/analysis/normed_space/exponential.lean#L559
ERR_LIN: Line has more than 100 characters
|
|
Lint style:
src/analysis/normed_space/exponential.lean#L571
ERR_LIN: Line has more than 100 characters
|
|
Lint style:
src/analysis/normed_space/exponential.lean#L578
ERR_LIN: Line has more than 100 characters
|
|
Lint style
Process completed with exit code 123.
|
|
Build mathlib
The run was canceled by @github-actions.
|
|
Build mathlib
The operation was canceled.
|
|
Build mathlib
Runner hoskinson3 did not respond to a cancelation request with 00:05:00.
|
Artifacts
Produced during runtime
| Name | Size | |
|---|---|---|
|
precompiled-mathlib-3.51.1-b275b43
Expired
|
403 MB |
|