Skip to content

introduce typo

introduce typo #22

Triggered via push September 26, 2024 16:27
Status Failure
Total duration 46s
Artifacts
Add topic label
39s
Add topic label
Fit to window
Zoom out
Zoom in

Annotations

2 errors
Misformatted `AutoLabel.mathlibLabels`: scripts/autolabel.lean#L1
scripts/autolabel.lean: directory 'Mathlib/LinearAlgebras' does not exist but is included by label 't-algebra'. Please update `AutoLabel.mathlibLabels`!
Add topic label
Process completed with exit code 2.