progress on golf #128621
build.yml
on: push
Cancel Previous Runs (CI)
4s
Post-CI job
0s
Annotations
4 errors
Lint style:
Mathlib/Order/CompleteLattice/Monovary.lean#L9
Mathlib/Order/CompleteLattice/Monovary.lean:9 ERR_MOD: Module docstring missing, or too late
|
Lint style
Process completed with exit code 1.
|
Build
The process '/usr/bin/env' failed with exit code 1
|
Build
The process '/usr/bin/bash' failed with exit code 1
|