]> https://gitweb.dealii.org/ - dealii.git/commitdiff
projects / dealii.git / commitdiff
? search:
summary | shortlog | log | commit | commitdiff | tree
raw | patch | inline | side by side (parent: f809d49)
set agent 7697/head
authorTimo Heister <timo.heister@gmail.com>
Tue, 5 Feb 2019 23:08:43 +0000 (16:08 -0700)
committerTimo Heister <timo.heister@gmail.com>
Tue, 5 Feb 2019 23:08:43 +0000 (16:08 -0700)
contrib/ci/Jenkinsfile.mark patch | blob | history

diff --git a/contrib/ci/Jenkinsfile.mark b/contrib/ci/Jenkinsfile.mark
index c10638a5133dbbf1c5057573d458c614dc02163e..37aa15478cd7de4dbc874585f20a7293aef81d05 100644 (file)
--- 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
   {
Mirror of the development repository for deal.II

In the beginning the Universe was created. This has made a lot of people very angry and has been widely regarded as a bad move.

Douglas Adams


Typeset in Trocchi and Trocchi Bold Sans Serif.