From 0f486d73e1304cc54714e8003ff721a7d1090432 Mon Sep 17 00:00:00 2001 From: retropikzel Date: Fri, 18 Apr 2025 08:29:23 +0300 Subject: [PATCH] Making the build work --- Jenkinsfile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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'