euprunin

Results 4 comments of euprunin

@zipfried Thanks! This seems to be working: ``` % git clone https://github.com/leanprover/fp-lean % cd fp-lean/ % cd examples/ % lake build % lake build subverso-extract-mod % cd ../book/ % lake...

When running `pandoc`, the only warnings that appear relate to 46 distinct characters that are missing from the specified font used: `[WARNING] Missing character: There is no […] in font...

Updated PDF generation instructions: ``` % git clone https://github.com/leanprover/fp-lean % cd fp-lean/examples/ % lake build % lake build subverso-extract-mod % cd ../book/ % lake exe fp-lean --with-html-single % pandoc _out/html-single/index.html...