diff options
| author | Enrico Tassi | 2015-02-04 11:30:56 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2015-02-04 11:30:56 +0100 |
| commit | d82daa51c47db9e9fdc24af74fb18d55e4adbc57 (patch) | |
| tree | 44539e60c5bd104cc6f51e2b1a1c5426c1dcd2d6 /lib | |
| parent | 8524f80ad30b744b66186cf59aec8d2524490da7 (diff) | |
Nativelib: catch Unix_error (like no ocamlopt found)
Diffstat (limited to 'lib')
0 files changed, 0 insertions, 0 deletions