diff options
| author | Gaëtan Gilbert | 2017-09-29 16:20:11 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2017-09-29 20:30:43 +0200 |
| commit | 0932339dbf44e4ef2b04426f7b4ac6d74b2f4f1f (patch) | |
| tree | 90057464a1a39f4d1de1af4193be6e6ebe998072 /engine/evd.mli | |
| parent | 95cd90c7e552b4362201abf671c68c5fbe950547 (diff) | |
Remove unused Failure catch
Unused since dc57718e98289b5d71a0a942d6a063d441dc6a54 as far as I can
tell.
Diffstat (limited to 'engine/evd.mli')
0 files changed, 0 insertions, 0 deletions