diff --git a/Jenkinsfile b/Jenkinsfile index f8dd71d..5984385 100644 --- a/Jenkinsfile +++ b/Jenkinsfile @@ -10,13 +10,6 @@ pipeline { stages { stage('chibi') { - agent { - dockerfile { - filename 'Dockerfile.test' - args '--user=root' - additionalBuildArgs "--build-arg COMPILE_R7RS=${STAGE_NAME}" - } - } environment { IMPLEMENTATION="${STAGE_NAME}" } @@ -25,7 +18,7 @@ pipeline { tests.each { test -> stage("${STAGE_NAME} ${test}") { catchError(buildResult: 'SUCCESS', stageResult: 'FAILURE') { - sh "make test-compile-r7rs COMPILE_R7RS=${env.IMPLEMENTATION} TESTNAME=${test}" + sh "make test-compile-r7rs-docker COMPILE_R7RS=${env.IMPLEMENTATION} TESTNAME=${test}" sh "cat tmp/test/primitives" } }