chore: adaptations for nightly-2024-10-19 #133714
kim-embuild.yml
on: push
Cancel Previous Runs (CI)
4s
Post-CI job
0s
Annotations
5 errors and 2 warnings
|
Build:
test/Lint.lean#L31
❌️ Docstring on `#guard_msgs` does not match generated message:
|
|
Build:
test/Lint.lean#L40
❌️ Docstring on `#guard_msgs` does not match generated message:
|
|
Build:
test/Lint.lean#L62
❌️ Docstring on `#guard_msgs` does not match generated message:
|
|
Build:
test/Lint.lean#L74
❌️ Docstring on `#guard_msgs` does not match generated message:
|
|
Build
The process '/home/lean/.elan/bin/lake' failed with exit code 1
|
|
Build:
test/Lint.lean#L76
The namespace 'add' is duplicated in the declaration 'add.add'
|
|
Build:
test/Lint.lean#L76
The namespace 'add' is duplicated in the declaration 'add.add'
|