Skip to content

fix: keep the space before a hygieneInfo antiquotation - #15025

Open
mhuisi wants to merge 1 commit into
leanprover:masterfrom
mhuisi:push-vnppputzlnsn
Open

fix: keep the space before a hygieneInfo antiquotation#15025
mhuisi wants to merge 1 commit into
leanprover:masterfrom
mhuisi:push-vnppputzlnsn

fix: keep the space before a `hygieneInfo` antiquotation

1d77f2b
Select commit
Loading
Failed to load commit list.
Sign in for the full log view
check-stdlib-flags
succeeded Sep 4, 2026 in 4s