PR summary c381ef07ce

Import changes for modified files

No significant changes to the import graph

Declarations diff

No declarations were harmed in the making of this PR! 🐙

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

I think that \'{\i} is also wrong (it does not render correctly in my WIP pure Lean bibtex diacritic parser leanprover/doc-gen4#200), it should be \'i. Any opinions?

I have removed the awaiting-review label according to the decision explained here
https://leanprover.zulipchat.com/#narrow/stream/113486-announce/topic/Changes.20to.20the.20.23queue/near/450176907

I have removed the awaiting-review label according to the decision explained here https://leanprover.zulipchat.com/#narrow/stream/113486-announce/topic/Changes.20to.20the.20.23queue/near/450176907

I see. Sorry for the inconvenience.

I think that \'{\i} is also wrong (it does not render correctly in my WIP pure Lean bibtex diacritic parser leanprover/doc-gen4#200), it should be \'i. Any opinions?

https://tex.stackexchange.com/q/409927/41112 suggests that the original is valid, but unnecessary in modern LaTeX.

bors merge

Thanks!

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style