![[Jenkins]](/ocaml/static/8707ff75/images/svgs/logo.svg){kind=logo}
Summary
- Use a pipeline to define the bootstrap Jenkins job, take #1 (commit: d0d8ace) (details)
| The file was added | tools/ci/inria/bootstrap/remove-sinh-primitive.patch |
| The file was added | tools/ci/inria/bootstrap/Jenkinsfile |
| The file was added | tools/ci/inria/bootstrap/script |
| The file was removed | tools/ci/inria/remove-sinh-primitive.patch |
| The file was removed | tools/ci/inria/bootstrap |