diff --git a/Jenkinsfile b/Jenkinsfile index 8b5ad77..1160a9b 100644 --- a/Jenkinsfile +++ b/Jenkinsfile @@ -8,7 +8,7 @@ pipeline { stages { stage('Chibi primitives') { - agent { dockerfile { filename 'Dockerfile.test', additionalBuildArgs '--build-arg COMPILE_R7RS=chibi' } } + agent { dockerfile { filename 'Dockerfile.test'; additionalBuildArgs '--build-arg COMPILE_R7RS=chibi' } } steps { catchError(buildResult: 'SUCCESS', stageResult: 'FAILURE') { sh 'make test-compile-r7rs COMPILE_R7RS=chibi TESTNAME=primitives' } } } }