diff options
| author | Linus Nordberg <linus@nordu.net> | 2015-11-10 16:31:54 +0100 |
|---|---|---|
| committer | Linus Nordberg <linus@nordu.net> | 2015-11-10 16:31:54 +0100 |
| commit | 3b1b80855704812d8f76fb3a258b52cee0d56720 (patch) | |
| tree | 6f9279cde3d1ece0ffa462cab888d844fe64d263 /tools/merge_sth.py | |
| parent | 274ea1a70ebe79800b2a3dc594363727ea306287 (diff) | |
Print the string "timing" and the name of the program in merge timing info.
Diffstat (limited to 'tools/merge_sth.py')
| -rwxr-xr-x | tools/merge_sth.py | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/merge_sth.py b/tools/merge_sth.py index bd49c9f..567082c 100755 --- a/tools/merge_sth.py +++ b/tools/merge_sth.py @@ -103,7 +103,7 @@ def merge_sth(args, config, localconfig): write_file(sthfile, sth) if args.timing: - print >>sys.stderr, timing["deltatimes"] + print >>sys.stderr, "timing: merge_sth:", timing["deltatimes"] sys.stderr.flush() def main(): |