4 ms·

Thanks for the tip! I think we already use xelatex, as the book is created with pandoc (https://pandoc.org/ https://pandoc.org/).