diff options
| author | Gereon Kremer <gereon.kremer@cs.rwth-aachen.de> | 2021-03-30 03:06:14 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-03-30 01:06:14 +0000 |
| commit | c7a8c32825af7dceb6cee631523a480a5b2cc6ba (patch) | |
| tree | 90393397cd0665fa72dbbe03f9cd4efa903faae1 /src/api | |
| parent | 7e5fe049ad88405a90fd5a43caa872d646d4b8e2 (diff) | |
Fix total time statistic (#6233)
Since one of the last changes to the total time collection in the driver, this collection fails when the solver terminates unexpectedly (either by a signal or an exception). This PR fixes this issue and does some cleanup along the way.
Diffstat (limited to 'src/api')
0 files changed, 0 insertions, 0 deletions