From: Daniel Arndt <arndtd@ornl.gov>
Date: Thu, 8 Dec 2022 15:56:43 +0000 (-0500)
Subject: Fix indentation in Jenkinsfile.mpi
X-Git-Tag: v9.5.0-rc1~751^2
X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=refs%2Fpull%2F14548%2Fhead;p=dealii.git

Fix indentation in Jenkinsfile.mpi
---

diff --git a/contrib/ci/Jenkinsfile.mpi b/contrib/ci/Jenkinsfile.mpi
index e54df7d7b1..948bd233c8 100644
--- 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'