mathlib3
93b41e56 - fix(*): put headings in multiline module docs on their own lines (#2742)

Commit
5 years ago
fix(*): put headings in multiline module docs on their own lines (#2742) found using regex: `/-! #([^-/])*$`. These don't render correctly in the mathlib docs. Module doc strings that consist of a heading on its own line are OK so I haven't changed them. I also moved some descriptive text from copyright headers to module docs, or removed such text if there was already a module doc string.
Parents
Loading