diff options
| author | Matthieu Sozeau | 2016-06-16 14:20:10 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2016-06-16 18:21:08 +0200 |
| commit | 0abade8ca36a68fbd90beb209de7647851416953 (patch) | |
| tree | 8f7875f9505bb5e3d91e55d9f71786e11a8bb27c /kernel/type_errors.mli | |
| parent | b0c84990af22e52e659bd2469af95ad2f39a047e (diff) | |
Tentative fix of test-suite file to avoid loop
Looping on jenkins only, couldn't reproduce locally.
To be investigated further.
Diffstat (limited to 'kernel/type_errors.mli')
0 files changed, 0 insertions, 0 deletions