Skip to content

ci: lint API maps#1436

Merged
jstoobysmith merged 2 commits into
leanprover-community:masterfrom
Robby955:api-map-lint
Jul 18, 2026
Merged

ci: lint API maps#1436
jstoobysmith merged 2 commits into
leanprover-community:masterfrom
Robby955:api-map-lint

ci: fix spelling in linter output

cb76b2f
Select commit
Loading
Failed to load commit list.
Sign in for the full log view

Annotations

1 warning
Python based linters
succeeded Jul 18, 2026 in 14s