diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-07-11 00:54:54 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-07-11 00:54:54 +0200 |
| commit | 8fead59914019aac5951ff123f806f69ceb30ccb (patch) | |
| tree | 89ac61d9783a3e0bf554a20f8177858498accf12 /.gitignore | |
| parent | b4572185522cd21e7e4e1cf59095ae66d0da0be1 (diff) | |
| parent | 70bf549f1c790969430f505c004b48637fef244e (diff) | |
Merge PR #8031: Remove auto-retry in GitLab CI now that @coqbot is handling it.
Diffstat (limited to '.gitignore')
0 files changed, 0 insertions, 0 deletions