+ /* 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_cfgelm_int, 1, 1, NULL, NULL);
+ xbt_cfg_setdefault_int(_sg_cfg_set, OPT_TRACING_PRECISION, 6);
+