216
219
if (DEBUG_STD) cout << "TeXmacs] Open pk " << name << "\n";
217
220
url u= resolve_tex (name);
221
227
if (get_setting ("MAKEPK") != "false") {
222
228
system_wait ("Generating font file", name);
223
229
make_tex_pk (family * size_name, dpi, as_int (get_setting ("DPI")));