idris-hackers/software-foundations

\idr{...} in headings is rendered poorly in ToC

yurrriq opened this issue · 3 comments

\idr{...} in headings is rendered poorly in ToC

The \subsection hack works well enough.

So should we just replace it with \subsection everywhere or you still hope to find a proper solution?

Both 😄