Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

Merge branch 'master' into YK-cont-alternating #121025

Merge branch 'master' into YK-cont-alternating

Merge branch 'master' into YK-cont-alternating #121025

Triggered via push November 28, 2023 16:02
Status Cancelled
Total duration 3m 11s
Artifacts
This run and associated checks have been archived and are scheduled for deletion. Learn more about checks retention

build.yml

on: push
Build mathlib
0s
Build mathlib
Cancel Previous Runs (CI)
4s
Cancel Previous Runs (CI)
Lint mathlib
0s
Lint mathlib
Run tests
0s
Run tests
Post-CI job
0s
Post-CI job
Fit to window
Zoom out
Zoom in

Annotations

5 errors
Lint style: src/topology/vector_bundle/alternating.lean#L162
ERR_LIN: Line has more than 100 characters
Lint style: src/analysis/normed_space/alternating.lean#L463
ERR_LIN: Line has more than 100 characters
Lint style: src/analysis/normed_space/alternating.lean#L464
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.