Define Inria CI's other-configs job as a Jenkins pipeline, take #2

master
Sébastien Hinderer 2020-08-14 15:50:25 +02:00
parent b1ffaf6008
commit 7b2689b8a0
1 changed files with 1 additions and 1 deletions

View File

@ -20,7 +20,7 @@
pipeline {
agent { label 'ocaml-linux-64' }
stages {
stage('Testing various other compiler configurations')
stage('Testing various other compiler configurations') {
steps {
sh 'tools/ci/inria/other-configs/script'
}