Fix an uncaught python exception in timing

Previously, when either the 'before' or 'after' had no files, we'd get
an uncaught exception:
```
Traceback (most recent call last):
  File "/home/jgross/Documents/repos/coq/tools/make-both-time-files.py", line 16, in <module>
    table = make_diff_table_string(left_dict, right_dict, sort_by=args.sort_by, include_mem=args.include_mem, sort_by_mem=args.sort_by_mem)
  File "/home/jgross/Documents/repos/coq/tools/TimeFileMaker.py", line 391, in make_diff_table_string
    right_peak = max(v.get(MEM_KEY, 0) for v in right_dict.values())
ValueError: max() arg is an empty sequence
```

Fixes #12387

1 files changed, 2 insertions, 2 deletions

diff --git a/tools/TimeFileMaker.py b/tools/TimeFileMaker.py
index a3078af4a1..12462726e5 100644
--- a/tools/TimeFileMaker.py
+++ b/tools/TimeFileMaker.py
@@ -387,8 +387,8 @@ def make_diff_table_string(left_dict, right_dict,
     total_string = 'Total' if not include_mem else 'Total Time / Peak Mem'
     middle_width = max(map(len, names + [tag, total_string]))
 
-    left_peak = max(v.get(MEM_KEY, 0) for v in left_dict.values())
-    right_peak = max(v.get(MEM_KEY, 0) for v in right_dict.values())
+    left_peak = max([0] + [v.get(MEM_KEY, 0) for v in left_dict.values()])
+    right_peak = max([0] + [v.get(MEM_KEY, 0) for v in right_dict.values()])
     diff_peak = left_peak - right_peak
     percent_diff_peak = (format_percentage((left_peak - right_peak) / float(right_peak))
                          if right_peak != 0 else (INFINITY if left_peak > 0 else 'N/A'))