aboutsummaryrefslogtreecommitdiff
path: root/kernel/nativelambda.mli
diff options
context:
space:
mode:
authorJason Gross2020-05-21 17:48:02 -0400
committerJason Gross2020-05-21 18:00:50 -0400
commit7731b8878d6a8c78874f6657745fa61d2703ee53 (patch)
tree96c18843022a5c9aa56efcc0a8f3e7e8a53d8b53 /kernel/nativelambda.mli
parent90389df4d03a6a6232e0372ff3efee720f85d284 (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