diff --git a/Jenkinsfile b/Jenkinsfile index bddc8fa..444b2ea 100644 --- a/Jenkinsfile +++ b/Jenkinsfile @@ -5,7 +5,7 @@ pipeline { } stages { stage("Build") { - agent { dockerfile { path 'Dockerfile'; args '--user=root --build-arg COMPILE_R7RS=sagittarius' } } + agent { dockerfile { filename 'Dockerfile'; args '--user=root --build-arg COMPILE_R7RS=sagittarius' } } steps { sh 'make' sh 'make install'