diff options
| author | Gaëtan Gilbert | 2019-05-16 13:15:12 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-05-17 14:33:28 +0200 |
| commit | be9a1834a48393185ec9cfd9c18d157fd2a7ff02 (patch) | |
| tree | 5f550b3a8655adeaa9686932bb12a850c3c13ce4 /plugins/micromega/persistent_cache.mli | |
| parent | e9c2bc9aaddd401d18d90411ff68644b1d05c0d5 (diff) | |
Fail: don't catch critical errors
Not sure why we didn't. Fail didn't catch anomalies almost by accident.
It still makes sense to catch Timeout here imo
Diffstat (limited to 'plugins/micromega/persistent_cache.mli')
0 files changed, 0 insertions, 0 deletions