Skip to content
continuous integration

Update Mathlib.lean #134921

Sign in to view logs

Update Mathlib.lean

Update Mathlib.lean #134921

Triggered via push October 24, 2024 02:32
@erdOneerdOne
pushed 15a3b87
erd1/immersion
Status Failure
Total duration 6m 52s
Artifacts –

build.yml

on: push
Lint style
1m 10s
Lint style
Build
6m 46s
Build
Cancel Previous Runs (CI)
2s
Cancel Previous Runs (CI)
Post-CI job
0s
Post-CI job
Fit to window
Zoom out
Zoom in

Annotations

3 errors
Build: Mathlib/AlgebraicGeometry/Morphisms/Immersion.lean#L49
@AlgebraicGeometry.Scheme.Hom.coborderRange definition missing documentation string
Build: Mathlib/AlgebraicGeometry/Morphisms/Immersion.lean#L53
@AlgebraicGeometry.Scheme.Hom.liftCoborder definition missing documentation string
Build
The process '/usr/bin/env' failed with exit code 1