int fontsTypewriterScale() const { return fonts_typewriter_scale[useNonTeXFonts]; }
/// the font used by the CJK command
std::string fonts_cjk;
int fontsTypewriterScale() const { return fonts_typewriter_scale[useNonTeXFonts]; }
/// the font used by the CJK command
std::string fonts_cjk;
bool track_changes;
/** This param decides whether change tracking marks should be used
* in output (irrespective of how these marks are actually defined;
* for instance, they may differ for DVI and PDF generation)
bool track_changes;
/** This param decides whether change tracking marks should be used
* in output (irrespective of how these marks are actually defined;
* for instance, they may differ for DVI and PDF generation)