Fix indentation in Jenkinsfile.mpi

diff --git a/contrib/ci/Jenkinsfile.mpi b/contrib/ci/Jenkinsfile.mpi
index e54df7d7b13e57da57182bb7a04a573b28486b9b..948bd233c870e51f8271f01acc9173a0fc92869b 100644 (file)
--- a/contrib/ci/Jenkinsfile.mpi
+++ b/contrib/ci/Jenkinsfile.mpi
@@ -57,12 +57,12 @@ pipeline
         {
           when {
             not {
-                   anyOf {
-                     branch 'master'
-                     branch pattern: "dealii-*", comparator: "GLOB"
-                   }
+              anyOf {
+                branch 'master'
+                branch pattern: "dealii-*", comparator: "GLOB"
+              }
             }
-               }
+          }
 
           steps
           {
@@ -124,7 +124,7 @@ pipeline
               sh "cp /home/dealii/build/detailed.log $WORKSPACE/detailed-mpi.log || true"
               archiveArtifacts artifacts: 'detailed-mpi.log', fingerprint: true
             }
-           
+
             failure
             {
               githubNotify context: 'Jenkins: MPI', description: 'build failed',  status: 'FAILURE'