diff options
| author | Emilio Jesus Gallego Arias | 2019-05-22 23:03:12 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-05-22 23:03:12 +0200 |
| commit | 20a464396fd89449569dc69b8cfb37cb69766733 (patch) | |
| tree | 0ee7ca0df404af94236829592765219c8213641a /plugins/micromega/persistent_cache.ml | |
| parent | 5c5bd952e9c28c3acf740fcdced03b2b7145076d (diff) | |
| parent | be9a1834a48393185ec9cfd9c18d157fd2a7ff02 (diff) | |
Merge PR #10173: Fail: don't catch critical errors
Diffstat (limited to 'plugins/micromega/persistent_cache.ml')
0 files changed, 0 insertions, 0 deletions