diff options
Diffstat (limited to 'tools/merge_dist.py')
| -rwxr-xr-x | tools/merge_dist.py | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/merge_dist.py b/tools/merge_dist.py index 05cffc2..9831f97 100755 --- a/tools/merge_dist.py +++ b/tools/merge_dist.py @@ -113,7 +113,7 @@ def merge_dist(args, localconfig, frontendnodes, timestamp): timing_point(timing, "send sth") if args.timing: - print >>sys.stderr, timing["deltatimes"] + print >>sys.stderr, "timing: merge_dist:", timing["deltatimes"] sys.stderr.flush() return timestamp |