diff options
| author | Enrico Tassi | 2017-06-20 15:18:40 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2017-06-20 15:49:44 +0200 |
| commit | 2e99ed199cde9495bd0f7e3c1209986bcaf77947 (patch) | |
| tree | 509d927c4cd2716494d3e6d123ed50496fd4f0b5 /API/API.mli | |
| parent | c68afe0da68a2653a47ac3ed2818886c1c338dda (diff) | |
STM: par: report no error to UIs in non-solve mode
Used to report to the UI an Error feedback message whenever a
worker was non making any progress. This is wrong since no-progress
is fine (as long as one does not specify "solve")
Diffstat (limited to 'API/API.mli')
0 files changed, 0 insertions, 0 deletions