]> https://gitweb.dealii.org/ - dealii.git/commitdiff
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

index c10638a5133dbbf1c5057573d458c614dc02163e..37aa15478cd7de4dbc874585f20a7293aef81d05 100644 (file)
@@ -20,7 +20,13 @@ Settings to apply inside Jenkins:
 
 pipeline
 {
-  agent none
+  agent
+  {
+    docker
+    {
+      image 'dealii/indent'
+    }
+  }
 
   stages
   {

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.