diff options
| -rw-r--r-- | tools/ci/inria/Risc-V/Jenkinsfile | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/ci/inria/Risc-V/Jenkinsfile b/tools/ci/inria/Risc-V/Jenkinsfile index 3cbf9e2884..4221adc373 100644 --- a/tools/ci/inria/Risc-V/Jenkinsfile +++ b/tools/ci/inria/Risc-V/Jenkinsfile @@ -26,7 +26,7 @@ pipeline { } } post { - always { + regression { emailext ( to: 'ocaml-ci-notifications@inria.fr', subject: 'Job $JOB_NAME $BUILD_STATUS (build #$BUILD_NUMBER)', |