Merge pull request #14548 from masterleinad/fix_indent_jenkins

Fix indentation in Jenkinsfile.mpi
dealii · Dec 8, 2022 · 70a5a9d · 70a5a9d
2 parents b8f4897 + 3a2ae57
commit 70a5a9d
Showing 1 changed file with 6 additions and 6 deletions.
diff --git 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'