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 /doc | |
| 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 'doc')
| -rw-r--r-- | doc/changelog/11-infrastructure-and-dependencies/12388-fix-timing-diff-0s.rst | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/doc/changelog/11-infrastructure-and-dependencies/12388-fix-timing-diff-0s.rst b/doc/changelog/11-infrastructure-and-dependencies/12388-fix-timing-diff-0s.rst new file mode 100644 index 0000000000..4e5406ad4d --- /dev/null +++ b/doc/changelog/11-infrastructure-and-dependencies/12388-fix-timing-diff-0s.rst @@ -0,0 +1,5 @@ +- **Fixed:** + ``make pretty-timed-diff`` no longer raises Python exceptions in the rare + corner case where the log of times contains no files (`#12388 + <https://github.com/coq/coq/pull/12388>`_, fixes `#12387 + <https://github.com/coq/coq/pull/12387>`_, by Jason Gross). |