diff options
| author | Pierre-Marie Pédrot | 2015-02-28 00:58:29 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-02-28 00:58:29 +0100 |
| commit | fcd7926fa8bddc86f66e936ad0bf615326b8cb6d (patch) | |
| tree | fb1be444a7b66b253e27c93b23eb229aacee0645 /stm | |
| parent | 2206b405c19940ca4ded2179d371c21fd13f1b6b (diff) | |
| parent | 78d1a61730886f89b01fa4245e58b54dd50fb4cf (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'stm')
| -rw-r--r-- | stm/stm.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/stm/stm.ml b/stm/stm.ml index 5edf480446..b38407c045 100644 --- a/stm/stm.ml +++ b/stm/stm.ml @@ -1067,7 +1067,7 @@ end = struct (* {{{ *) ignore(Future.join checked_proof); RespBuiltProof(proof,time) with - | e when Errors.noncritical e -> + | e when Errors.noncritical e || e = Stack_overflow -> let (e, info) = Errors.push e in (* This can happen if the proof is broken. The error has also been * signalled as a feedback, hence we can silently recover *) |