idris-hackers/software-foundations

Doubles of certain special characters

tsani opened this issue · 1 comments

tsani commented

Some special characters are duplicated in the output. In particular,

  • %
  • #

Both are special in LaTeX, which is why I suspect this is happening.

yurrriq commented

Thanks, nice catch!