From a1e4ce9bbe4a92b71b09add8df2efd75626c44ed Mon Sep 17 00:00:00 2001 From: Timo Heister Date: Tue, 5 Feb 2019 16:08:43 -0700 Subject: [PATCH] set agent --- contrib/ci/Jenkinsfile.mark | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/contrib/ci/Jenkinsfile.mark b/contrib/ci/Jenkinsfile.mark index c10638a513..37aa15478c 100644 --- a/contrib/ci/Jenkinsfile.mark +++ b/contrib/ci/Jenkinsfile.mark @@ -20,7 +20,13 @@ Settings to apply inside Jenkins: pipeline { - agent none + agent + { + docker + { + image 'dealii/indent' + } + } stages { -- 2.39.5