diff options
| author | Emilio Jesus Gallego Arias | 2019-08-08 22:02:46 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-08-08 22:02:46 +0200 |
| commit | 0146ca2b11a255cbfe2868923b80376a61cc05de (patch) | |
| tree | ae7a1fcc3fd55b69574dc51561e6dc369654e781 /plugins/extraction/mlutil.ml | |
| parent | 9fdeb13166af29bfc6ec1e1930f1932ddc9f1cd4 (diff) | |
| parent | 86e8deed878251e74534393a7b37a1471f7fa079 (diff) | |
Merge PR #10639: map directory read error to empty directory
Reviewed-by: ejgallego
Diffstat (limited to 'plugins/extraction/mlutil.ml')
0 files changed, 0 insertions, 0 deletions