Skip to content

fix: gracefully handle unknown -D options in verso-literate - #969

Open
mo271 wants to merge 1 commit into
leanprover:mainfrom
mo271:weak_fix
Open

fix: gracefully handle unknown -D options in verso-literate#969
mo271 wants to merge 1 commit into
leanprover:mainfrom
mo271:weak_fix

Commits

Commits on Aug 21, 2026