From: Timo Heister <timo.heister@gmail.com>
Date: Thu, 8 Dec 2022 00:14:05 +0000 (-0500)
Subject: indent
X-Git-Tag: v9.5.0-rc1~752^2
X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=refs%2Fpull%2F14542%2Fhead;p=dealii.git

indent
---

diff --git a/contrib/ci/Jenkinsfile.mpi b/contrib/ci/Jenkinsfile.mpi
index f891c71b13..e54df7d7b1 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
           {