diff options
| author | Emilio Jesus Gallego Arias | 2019-04-03 17:18:19 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-04-03 17:18:19 +0200 |
| commit | 4a42b2cf7f0c67370a329fe626d0e49264564302 (patch) | |
| tree | 146416f8b43c7266027b69730413f9751934ef4e /stm/asyncTaskQueue.ml | |
| parent | fe24cd51c5cd816bdda2ab7ea590014afe27b863 (diff) | |
| parent | c078bebdf041b072590b69b1c4a64cb588f97499 (diff) | |
Merge PR #9804: CI: Use job-local timeout for build-template and test-suite-template
Reviewed-by: ejgallego
Reviewed-by: gares
Diffstat (limited to 'stm/asyncTaskQueue.ml')
0 files changed, 0 insertions, 0 deletions