From: Timo Heister <timo.heister@gmail.com>
Date: Tue, 5 Feb 2019 23:08:43 +0000 (-0700)
Subject: set agent
X-Git-Tag: v9.1.0-rc1~363^2
X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=a1e4ce9bbe4a92b71b09add8df2efd75626c44ed;p=dealii.git

set agent
---

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
   {