- String id_str = "Lily was here";
- if (no_timestamps_global_b)
- id_str += ".";
- else
- id_str += String (", ") + get_version_str ();
- output_String_def ( "LilyIdString", id_str);
-}
-
-void
-Paper_outputter::switch_to_font (String fontname)
-{
- if (fontname.length_i () && fontname != current_font_)
- {
- current_font_ = fontname;
- int i=0;
-
- for (; i< font_arr_.size (); i++)
- if (font_arr_[i] == fontname)
- break;
-
- if (i == font_arr_.size ())
- {
- font_arr_.push (fontname);
- output_font_def (i, fontname);
- }
- output_font_switch (i);
- }
- return;
-}
+ String id_string = "Lily was here";
+ id_string += String_convert::pad_to (String (", ") + version_string (), 40);