diff options
| author | Maxime Dénès | 2017-06-16 17:13:45 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-06-16 17:13:45 +0200 |
| commit | 52ab54dc6734319203442f36de4d7ddd4fd999b9 (patch) | |
| tree | f86178325dd95e71252c034676d22df7fd1d0bde /API/API.ml | |
| parent | db522eb68496f56c11d43cb269c4d14943f334af (diff) | |
| parent | f70f12b56e44abd9df4ad6941ee4941a761302fa (diff) | |
Merge PR#804: Increase the time limit on 4366.v to make gitlab work better.
Diffstat (limited to 'API/API.ml')
0 files changed, 0 insertions, 0 deletions