-
Committer:
Alberto Garcia
-
Date:
2018-02-12 15:41:16 UTC
-
Revision ID:
albertog@icmab.es-20180212154116-6u0tvxmsbnayrsjf
Write JSON file for tree-timer information
A more flexible output for timing information.
The 'time.json' file is produced if the option
use-tree-timer T
is in effect.