Skip to content

more, and still more to go #89913

more, and still more to go

more, and still more to go #89913

Triggered via push May 8, 2024 12:32
Status Failure
Total duration 12m 27s
Artifacts

build.yml

on: push
Cancel Previous Runs (CI)
3s
Cancel Previous Runs (CI)
check workflows
11s
check workflows
Post-CI job
0s
Post-CI job
Fit to window
Zoom out
Zoom in

Annotations

4 errors
Lint style: Mathlib/Analysis/NormedSpace/HahnBanach/Extension.lean#L90
Mathlib/Analysis/NormedSpace/HahnBanach/Extension.lean:90 ERR_LIN: Line has more than 100 characters
Lint style
Process completed with exit code 123.
Build
The process '/usr/bin/env' failed with exit code 1
Build
The process '/usr/bin/bash' failed with exit code 1