array_append_format (args, "GPRINT:vdef_%04i_min:%%lg min,", index);
array_append_format (args, "GPRINT:vdef_%04i_avg:%%lg avg,", index);
array_append_format (args, "GPRINT:vdef_%04i_max:%%lg max,", index);
array_append_format (args, "GPRINT:vdef_%04i_min:%%lg min,", index);
array_append_format (args, "GPRINT:vdef_%04i_avg:%%lg avg,", index);
array_append_format (args, "GPRINT:vdef_%04i_max:%%lg max,", index);