Skip to content

chore: drop no-op @[expose] on optionDocs.Args - #906

Merged
robsimmons merged 1 commit into
leanprover:mainfrom
kim-em:chore/drop-noop-expose-optiondocs
Jul 7, 2026
Merged

chore: drop no-op @[expose] on optionDocs.Args#906
robsimmons merged 1 commit into
leanprover:mainfrom
kim-em:chore/drop-noop-expose-optiondocs

Commits

Commits on Jul 6, 2026