xbt_cfg_setdefault_string(_sg_cfg_set, OPT_TRACING_COMMENT_FILE, "");
/* trace timestamp precision */
xbt_cfg_register(&_sg_cfg_set, OPT_TRACING_PRECISION,
"Numerical precision used when timestamping events (hence this value is expressed in number of digits after decimal point)",
xbt_cfg_setdefault_string(_sg_cfg_set, OPT_TRACING_COMMENT_FILE, "");
/* trace timestamp precision */
xbt_cfg_register(&_sg_cfg_set, OPT_TRACING_PRECISION,
"Numerical precision used when timestamping events (hence this value is expressed in number of digits after decimal point)",