diff options
| author | Jason Gross | 2020-05-21 17:48:02 -0400 |
|---|---|---|
| committer | Jason Gross | 2020-05-21 18:00:50 -0400 |
| commit | 7731b8878d6a8c78874f6657745fa61d2703ee53 (patch) | |
| tree | 96c18843022a5c9aa56efcc0a8f3e7e8a53d8b53 /kernel/nativelambda.mli | |
| parent | 90389df4d03a6a6232e0372ff3efee720f85d284 (diff) | |
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
Diffstat (limited to 'kernel/nativelambda.mli')
0 files changed, 0 insertions, 0 deletions
